proposition: Lemma lucastest_bounded x p1 : 0 <= [|x|] < [|b|] -> 0 <= [|lucastest_step x p1|] < [|b|].
proof: Proof. unfold lucastest_step. revert p1 x. intros p1; pattern p1; apply Pind; simpl iter_pos; simpl s; clear p1. exact square_m2_bounded. intros p1 IH x Hx. rewrite Pos.iter_succ. apply square_m2_bounded. apply IH; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits