proposition: Theorem Fermat_pos: forall n, 1 < FermatNumber n.
proof: Proof. unfold FermatNumber; intros n. solve [ auto with zarith | (apply Z.le_lt_trans with (2 ^ 2 ^(Z_of_nat n)); auto with zarith; rewrite <- (Zpower_0_r 2); auto with zarith; apply Zpower_le_monotone; try split; auto with zarith)]. Qed.
imports: ZArith ZCAux Pocklington