proposition: Lemma _sub_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> [|_sub_mod w1 w2|] = ([|w1|] - [|w2|]) mod [|b|].
proof: Proof. intros w2 w3 t1 t2; unfold _sub_mod, w_compare, w_sub_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.sub_c ?x ?y] => generalize (ZnZ.spec_sub_c x y); unfold interp_carry; case (ZnZ.sub_c x y); autorewrite with w_rewrite end; auto with zarith. intros w4 H2. rewrite Zmod_small; auto with zarith. split; auto with zarith. rewrite <- H2; case (ZnZ.spec_to_Z w4); auto with zarith. apply Z.le_lt_trans with [|w2|]; auto with zarith. case (ZnZ.spec_to_Z w3); auto with zarith. intros w4 H2; rewrite <- H2. unfold w_add; rewrite ZnZ.spec_add; auto with zarith. case (ZnZ.spec_to_Z w4); intros F1 F2. assert (F3: 0 <= - 1 * base (ZnZ.digits w_op) + [|w4|] + [|b|]); auto with zarith. rewrite H2. case (ZnZ.spec_to_Z w3); case (ZnZ.spec_to_Z w2); auto with zarith. rewrite <- (fun x => Zmod_minus_one ([|w4|] + x)); auto with zarith. rewrite <- (fun x y => Zmod_plus_one (-y + x)); auto with zarith. repeat rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z b); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux