proposition: Theorem lucas_prime: forall p, 2 < Zpos p -> lucas p = 0 -> prime (2 ^ Zpos p - 1).
proof: Proof. intros p Hp H. assert(A1: ZnZ.Specs (op p)). apply cmk_spec; auto. apply (lucastest_prime A1 Hp (lucas_f2 Hp) (lucas_f3 Hp) H). Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits