proposition: Theorem lucastest_prop: lucastest = fst(s (Zpos p -2)) mod (2 ^ Zpos p - 1).
proof: Proof. unfold lucastest. assert (F: 0 <= 0); auto with zarith. generalize (lucastest_step_correct (p -2) w4 F); simpl Zplus; rewrite Zpos_minus; auto with zarith. rewrite Zmax_right; auto with zarith. intros tmp; apply tmp; clear tmp. rewrite <- b_p; simpl; exact w4_b. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits