proposition: Theorem LucasTest: forall n, lucas_test n = true -> prime (Mp n).
proof: Proof. intros n; unfold lucas_test; case (Z_lt_dec 2 n); intros H1; try (intros; discriminate). case (Z.eq_dec (SS n) 0); intros H2; try (intros; discriminate). intros _; apply LucasLehmer; auto. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup