proposition: Lemma square_m2_bounded x : 0 <= [|x|] < [|b|] -> 0 <= [|square_m2 x|] < [|b|].
proof: Proof. intro H. unfold square_m2. rewrite (sub_mod_spec m_op_spec _ _ [|square_mod m_op x|] 2). apply Z.mod_pos_bound; auto with zarith. rewrite Z.mod_small; auto with zarith. rewrite (square_mod_spec m_op_spec x [|x|]); auto. apply Z.mod_pos_bound; auto with zarith. rewrite Z.mod_small; auto with zarith. exact w2_b. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits