proposition: Lemma _msquare_mod_spec: forall w1 t1, [|w1|] = t1 mod [|b|] -> [|_msquare_mod w1|] = ([|w1|] * [|w1|]) mod [|b|].
proof: Proof. intros w2 t2; unfold _msquare_mod, w_square_c; intros H. assert (F: [|w2|] < [|b|]). case (Z_mod_lt t2 [|b|]); auto with zarith. match goal with |- context[ZnZ.square_c ?x] => generalize (ZnZ.spec_square_c x); unfold interp_carry; case (ZnZ.square_c x); autorewrite with w_rewrite end; auto with zarith. simpl; intros H2; rewrite <- H2; rewrite Zmod_small; auto with zarith. intros w4 w5 H2. rewrite mmul_aux5; auto with zarith. unfold ww_to_Z, w_to_Z ,w_digits; rewrite <- H2; auto. unfold ww_to_Z,w_to_Z ,w_digits; rewrite H2. apply Zmult_lt_compat; auto with zarith. case (ZnZ.spec_to_Z w2); auto with zarith. case (ZnZ.spec_to_Z w2); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux