Euler n <> 0 by PEPIN:42;
hence Euler n is positive ; :: thesis: verum