proposition: Lemma _add_mod_correct: forall w1 w2, [|w1|] + [|w2|] < 2 * [|b|] -> [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|].
proof: Proof. intros w2 w3; unfold _add_mod, w_compare, w_add_c; intros H. match goal with |- context[ZnZ.add_c ?x ?y] => generalize (ZnZ.spec_add_c x y); unfold interp_carry; case (ZnZ.add_c x y); autorewrite with w_rewrite end; auto with zarith. intros w4 H2. rewrite ZnZ.spec_compare; case Z.compare_spec; intros H1; match goal with H: context[b] |- _ => generalize H; clear H; intros H1; rewrite <-H2; auto with zarith end. rewrite H1, Z_mod_same; auto with zarith. rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z w4); auto with zarith. assert (F1: 0 < [|w4|] - [|b|]); auto with zarith. assert (F2: [|w4|] < [|b|] + [|b|]); auto with zarith. autorewrite with w_rewrite; auto. rewrite (fun x y => Zmod_small (x - y)); auto with zarith. rewrite <- (Zmod_minus_one [|w4|]); auto with zarith. apply sym_equal; apply Zmod_small; auto with zarith. split; auto with zarith. apply Z.lt_trans with [|b|]; auto with zarith. case (ZnZ.spec_to_Z b); unfold base; auto with zarith. rewrite Zmult_1_l; intros w4 H2; rewrite <- H2. unfold mb, w_add; rewrite ZnZ.spec_add; auto with zarith. assert (F1: [|w4|] < [|b|]). assert (F2: base (ZnZ.digits w_op) + [|w4|] < base (ZnZ.digits w_op) + [|b|]); auto with zarith. rewrite H2. apply Z.lt_trans with ([|b|] +[|b|]); auto with zarith. apply Zplus_lt_compat_r; auto with zarith. case (ZnZ.spec_to_Z b); auto with zarith. assert (F2: [|b|] < base (ZnZ.digits w_op) + [|w4|]); auto with zarith. apply Z.lt_le_trans with (base (ZnZ.digits w_op)); auto with zarith. case (ZnZ.spec_to_Z b); auto with zarith. case (ZnZ.spec_to_Z w4); auto with zarith. assert (F3: base (ZnZ.digits w_op) + [|w4|] < [|b|] + [|b|]); auto with zarith. rewrite <- (fun x => Zmod_minus_one (base x + [|w4|])); auto with zarith. rewrite (fun x y => Zmod_small (x - y)); auto with zarith. unfold w_opp;rewrite (ZnZ.spec_opp b). rewrite <- (fun x => Zmod_plus_one (-x)); auto with zarith. rewrite (Zmod_small (- [|b|] + base (ZnZ.digits w_op)));auto with zarith. 2 : assert (HHH := ZnZ.spec_to_Z b);auto with zarith. repeat rewrite Zmod_small; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux