proposition: Theorem lucastest_prime: lucastest = 0 -> prime (2 ^ Zpos p - 1).
proof: Proof. intros H1; case (prime_dec (2 ^ Zpos p - 1)); auto; intros H2. case Zdivide_div_prime_le_square with (2 := H2). assert (H3: 2 ^ 1 < 2 ^ Zpos p). apply Zpower_lt_monotone; auto with zarith. rewrite Zpower_1_r in H3; auto with zarith. intros q (H3, (H4, H5)). contradict H5; apply Zlt_not_le. generalize q_more_than_square; unfold Mp; intros tmp; apply tmp; auto; clear tmp. apply lucastest_prop_cor; auto. case (Zle_lt_or_eq 2 q); auto. apply prime_ge_2; auto. intros H5; subst. absurd (2 <= 1); auto with arith. apply Zdivide_le; auto with zarith. case H4; intros x Hx. exists (2 ^ (Zpos p -1) - x). rewrite Zmult_minus_distr_r; rewrite <- Hx; unfold Mp. pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith. replace (Zpos p - 1 + 1) with (Zpos p); auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits