proposition: Theorem ProthTestOp: forall h k a, proth_test h k a = true -> prime (h * 2 ^ k + 1).
proof: Proof. intros h k a; unfold proth_test. repeat match goal with |- context[if ?X then _ else _] => case X end; try (intros; discriminate). intros H1 H2 H3 H4 _. assert (Hu: 0 < h * 2 ^ k). apply Zmult_lt_O_compat; auto with zarith. apply ProthTest with (a := a); auto. rewrite Zplus_mod; auto with zarith. rewrite <- Zpow_mod_Zpower_correct; auto with zarith. rewrite H1. rewrite (Zmod_small 1); auto with zarith. replace (h * 2 ^ k + 1 - 1 + 1) with (h * 2 ^ k + 1); auto with zarith. apply Zdivide_mod; auto with zarith. apply Z_div_pos; auto with zarith. Qed.
imports: ZArith ZCAux Pocklington