proposition: Lemma _add_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|].
proof: Proof. intros w2 w3 t1 t2 H H1. apply _add_mod_correct; auto with zarith. 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. assert (tmp: forall x, 2 * x = x + x); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux