proposition: Lemma square_m2_eq x1 x2 : [|x1|] < [|b|] -> [|x1|] = [|x2|] -> [|square_m2 x1|] = [|square_m2 x2|].
proof: Proof. intros Hx1 Ex1. assert (H1 : [|x1|] = [|x1|] mod [|b|]). rewrite Z.mod_small; auto with zarith. case (ZnZ.spec_to_Z x1); auto with zarith. assert (H2 : [|x2|] = [|x2|] mod [|b|]). rewrite <- Ex1; auto. unfold square_m2. rewrite (sub_mod_spec m_op_spec _ _ [|square_mod m_op x1|] 2). rewrite (sub_mod_spec m_op_spec _ _ [|square_mod m_op x2|] 2). rewrite (square_mod_spec m_op_spec x1 [|x1|]); auto. rewrite (square_mod_spec m_op_spec x2 [|x2|]); auto. rewrite Ex1; auto. rewrite Z.mod_small; auto with zarith. rewrite (square_mod_spec m_op_spec x2 [|x2|]); auto. apply Z.mod_bound_pos; auto with zarith. apply Z.square_nonneg. exact w2_b. rewrite Z.mod_small; auto with zarith. rewrite (square_mod_spec m_op_spec x1 [|x1|]); auto. apply Z.mod_bound_pos; auto with zarith. apply Z.square_nonneg. exact w2_b. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits