proposition: Lemma _mmul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> [|_mmul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|].
proof: Proof. intros w2 w3 t1 t2; unfold _mmul_mod, w_mul_c; intros H H1. assert (F: [|w2|] < [|b|]). case (Z_mod_lt t1 [|b|]); auto with zarith. assert (F': [|w3|] < [|b|]). case (Z_mod_lt t2 [|b|]); auto with zarith. match goal with |- context[ZnZ.mul_c ?x ?y] => generalize (ZnZ.spec_mul_c x y); unfold interp_carry; case (ZnZ.mul_c x y); 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. rewrite <- H2; auto. unfold ww_to_Z,w_digits,w_to_Z; rewrite H2. apply Zmult_lt_compat; auto with zarith. case (ZnZ.spec_to_Z w2); auto with zarith. case (ZnZ.spec_to_Z w3); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux