proposition: Lemma lucastest_eq x1 x2 p1 : [|x1|] < [|b|] -> [|x1|] = [|x2|] -> [|lucastest_step x1 p1|] = [|lucastest_step x2 p1|].
proof: Proof. unfold lucastest_step. revert p1 x1 x2. intros p1; pattern p1; apply Pind; simpl iter_pos; simpl s; clear p1. exact square_m2_eq. intros p1 IH x1 x2 Hx1 Hx2. rewrite !Pos.iter_succ. apply square_m2_eq. assert (F : 0 <= [|x1|] < [|b|]). case (ZnZ.spec_to_Z x1); auto with zarith. generalize (lucastest_bounded _ p1 F). unfold lucastest_step; auto with zarith. apply IH; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits