proposition: Theorem lucastest_step_add : forall p1 p2 z z1 z2, lucastest_step z p1 = z1 -> lucastest_step z1 p2 = z2 -> lucastest_step z (p2 + p1) = z2.
proof: Proof. unfold lucastest_step. intros p1 p2 z z1 z2 H1 H2. rewrite Pos.iter_add, H1; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits