proposition: Theorem lucastest_prop_cor: lucastest = 0 -> (2 ^ Zpos p - 1 | fst(s (Zpos p - 2)))%Z.
proof: Proof. intros H. apply Zmod_divide. assert (H1: 2 ^ 1 < 2 ^ Zpos p). apply Zpower_lt_monotone; auto with zarith. rewrite Zpower_1_r in H1; auto with zarith. apply trans_equal with (2:= H); apply sym_equal; apply lucastest_prop; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits