proposition: Theorem PepinTestOp: forall n, pepin_test n = true -> prime (FermatNumber n).
proof: Proof. intros n; unfold pepin_test. match goal with |- context[if ?X then _ else _] => case X end; try (intros; discriminate). intros H1 _; apply PepinTest. generalize (Fermat_pos n); intros H2. rewrite Zplus_mod; auto with zarith. rewrite <- Zpow_mod_Zpower_correct; auto with zarith. rewrite H1. rewrite (Zmod_small 1); auto with zarith. replace (FermatNumber n - 1 + 1) with (FermatNumber n); auto with zarith. apply Zdivide_mod; auto with zarith. apply Z_div_pos; auto with zarith. Qed.
imports: ZArith ZCAux Pocklington