proposition: Lemma isM2_correct: forall p, if isM2 p then ~(Z.divide 2 p) /\ 2 < p else True.
proof: Proof. intros p; case p; simpl; auto; clear p. intros p1; split; auto. intros HH; inversion_clear HH. generalize H; rewrite Zmult_comm. case x; simpl; intros; discriminate. case p1; red; simpl; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod