proposition: Lemma lucas_step_same_p : forall p x p1 p2 z, p1 = p2 -> lucas_step p x p1 = z -> lucas_step p x p2 = z.
proof: Proof. intros p x p1 p2 z Hp Hz. apply trans_equal with (2 := Hz). apply f_equal2 with (f := lucas_step p); auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits