proposition: Theorem LucasLehmer: forall p, 2 < p -> SS p = 0 -> prime (Mp p).
proof: Proof. intros p H H1; case (prime_dec (Mp p)); auto; intros H2. case Zdivide_div_prime_le_square with (2 := H2). apply mersenne_pos; apply Z.lt_trans with 2; auto with zarith. intros q (H3, (H4, H5)). contradict H5; apply Zlt_not_le. apply q_more_than_square; auto. apply SS_prop_cor; auto. apply Z.lt_trans with 2; auto with zarith. 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 ^ (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 (p - 1 + 1) with p; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup