Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 465 insertions, 472 deletions

diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index b167b6ef9..37d987855 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -13,9 +13,8 @@
 (*                                                        *)
 (**********************************************************)
 
-Require Rbase.
-Require Omega.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Omega.
 Open Local Scope R_scope.
 
 (*********************************************************)
@@ -23,83 +22,81 @@ Open Local Scope R_scope.
 (*********************************************************)
 
 (**********)
-Definition Int_part:R->Z:=[r:R](`(up r)-1`).
+Definition Int_part (r:R) : Z := (up r - 1)%Z.
 
 (**********)
-Definition frac_part:R->R:=[r:R](Rminus r (IZR (Int_part r))).
+Definition frac_part (r:R) : R := r - IZR (Int_part r).
 
 (**********)
-Lemma tech_up:(r:R)(z:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1))->
-  z=(up r).
-Intros;Generalize (archimed r);Intro;Elim H1;Intros;Clear H1;
- Unfold Rgt in H2;Unfold Rminus in H3;
-Generalize (Rle_compatibility r (Rplus (IZR (up r)) 
- (Ropp r)) R1 H3);Intro;Clear H3;
- Rewrite (Rplus_sym (IZR (up r)) (Ropp r)) in H1;
- Rewrite <-(Rplus_assoc r (Ropp r) (IZR (up r))) in H1;
- Rewrite (Rplus_Ropp_r r) in H1;Elim (Rplus_ne (IZR (up r)));Intros a b;
- Rewrite b in H1;Clear a b;Apply (single_z_r_R1 r z (up r));Auto with zarith real.
+Lemma tech_up : forall (r:R) (z:Z), r < IZR z -> IZR z <= r + 1 -> z = up r.
+intros; generalize (archimed r); intro; elim H1; intros; clear H1;
+ unfold Rgt in H2; unfold Rminus in H3;
+ generalize (Rplus_le_compat_l r (IZR (up r) + - r) 1 H3); 
+ intro; clear H3; rewrite (Rplus_comm (IZR (up r)) (- r)) in H1;
+ rewrite <- (Rplus_assoc r (- r) (IZR (up r))) in H1;
+ rewrite (Rplus_opp_r r) in H1; elim (Rplus_ne (IZR (up r))); 
+ intros a b; rewrite b in H1; clear a b; apply (single_z_r_R1 r z (up r));
+ auto with zarith real.
 Qed.
 
 (**********)
-Lemma up_tech:(r:R)(z:Z)(Rle (IZR z) r)->(Rlt r (IZR `z+1`))->
-  `z+1`=(up r).
-Intros;Generalize (Rle_compatibility R1 (IZR z) r H);Intro;Clear H;
- Rewrite (Rplus_sym R1 (IZR z)) in H1;Rewrite (Rplus_sym R1 r) in H1;
- Cut (R1==(IZR `1`));Auto with zarith real.
-Intro;Generalize H1;Pattern 1 R1;Rewrite H;Intro;Clear H H1;
- Rewrite <-(plus_IZR z `1`) in H2;Apply (tech_up r `z+1`);Auto with zarith real.
+Lemma up_tech :
+ forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r.
+intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H;
+ rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1;
+ cut (1 = IZR 1); auto with zarith real.
+intro; generalize H1; pattern 1 at 1 in |- *; rewrite H; intro; clear H H1;
+ rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1));
+ auto with zarith real.
 Qed.
 
 (**********)
-Lemma fp_R0:(frac_part R0)==R0.
-Unfold frac_part; Unfold Int_part; Elim (archimed R0);
- Intros; Unfold Rminus;
- Elim (Rplus_ne (Ropp (IZR `(up R0)-1`))); Intros a b;
- Rewrite b;Clear a b;Rewrite <- Z_R_minus;Cut (up R0)=`1`.
-Intro;Rewrite H1;
- Rewrite (eq_Rminus (IZR `1`) (IZR `1`) (refl_eqT R (IZR `1`)));
- Apply Ropp_O. 
-Elim (archimed R0);Intros;Clear H2;Unfold Rgt in H1;
- Rewrite (minus_R0 (IZR (up R0))) in H0;
- Generalize (lt_O_IZR (up R0) H1);Intro;Clear H1;
- Generalize (le_IZR_R1 (up R0) H0);Intro;Clear H H0;Omega.
+Lemma fp_R0 : frac_part 0 = 0.
+unfold frac_part in |- *; unfold Int_part in |- *; elim (archimed 0); intros;
+ unfold Rminus in |- *; elim (Rplus_ne (- IZR (up 0 - 1))); 
+ intros a b; rewrite b; clear a b; rewrite <- Z_R_minus; 
+ cut (up 0 = 1%Z).
+intro; rewrite H1;
+ rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (refl_equal (IZR 1))); 
+ apply Ropp_0. 
+elim (archimed 0); intros; clear H2; unfold Rgt in H1;
+ rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1);
+ intro; clear H1; generalize (le_IZR_R1 (up 0) H0); 
+ intro; clear H H0; omega.
 Qed.
 
 (**********)
-Lemma for_base_fp:(r:R)(Rgt (Rminus (IZR (up r)) r) R0)/\ 
-                       (Rle (Rminus (IZR (up r)) r) R1).
-Intro; Split;
- Cut (Rgt (IZR (up r)) r)/\(Rle (Rminus (IZR (up r)) r) R1).
-Intro; Elim H; Intros.
-Apply (Rgt_minus (IZR (up r)) r H0).
-Apply archimed.
-Intro; Elim H; Intros.
-Exact H1.
-Apply archimed.
+Lemma for_base_fp : forall r:R, IZR (up r) - r > 0 /\ IZR (up r) - r <= 1.
+intro; split; cut (IZR (up r) > r /\ IZR (up r) - r <= 1).
+intro; elim H; intros.
+apply (Rgt_minus (IZR (up r)) r H0).
+apply archimed.
+intro; elim H; intros.
+exact H1.
+apply archimed.
 Qed.
 
 (**********)
-Lemma base_fp:(r:R)(Rge (frac_part r) R0)/\(Rlt (frac_part r) R1).
-Intro; Unfold frac_part; Unfold Int_part; Split.
+Lemma base_fp : forall r:R, frac_part r >= 0 /\ frac_part r < 1.
+intro; unfold frac_part in |- *; unfold Int_part in |- *; split.
      (*sup a O*)
-Cut (Rge (Rminus r (IZR (up r))) (Ropp R1)).
-Rewrite <- Z_R_minus;Simpl;Intro; Unfold Rminus;
- Rewrite Ropp_distr1;Rewrite <-Rplus_assoc;
- Fold (Rminus r (IZR (up r)));
- Fold (Rminus (Rminus r (IZR (up r))) (Ropp R1));
- Apply Rge_minus;Auto with zarith real.
-Rewrite <- Ropp_distr2;Apply Rle_Ropp;Elim (for_base_fp r); Auto with zarith real.
+cut (r - IZR (up r) >= -1).
+rewrite <- Z_R_minus; simpl in |- *; intro; unfold Rminus in |- *;
+ rewrite Ropp_plus_distr; rewrite <- Rplus_assoc;
+ fold (r - IZR (up r)) in |- *; fold (r - IZR (up r) - -1) in |- *;
+ apply Rge_minus; auto with zarith real.
+rewrite <- Ropp_minus_distr; apply Ropp_le_ge_contravar; elim (for_base_fp r);
+ auto with zarith real.
     (*inf a 1*) 
-Cut (Rlt (Rminus r (IZR (up r))) R0).
-Rewrite <- Z_R_minus; Simpl;Intro; Unfold Rminus;
- Rewrite Ropp_distr1;Rewrite <-Rplus_assoc;
- Fold (Rminus r (IZR (up r)));Rewrite Ropp_Ropp;
- Elim (Rplus_ne R1);Intros a b;Pattern 2 R1;Rewrite <-a;Clear a b;
- Rewrite (Rplus_sym  (Rminus r (IZR (up r))) R1);
- Apply Rlt_compatibility;Auto with zarith real.
-Elim (for_base_fp r);Intros;Rewrite <-Ropp_O;
- Rewrite<-Ropp_distr2;Apply Rgt_Ropp;Auto with zarith real.
+cut (r - IZR (up r) < 0).
+rewrite <- Z_R_minus; simpl in |- *; intro; unfold Rminus in |- *;
+ rewrite Ropp_plus_distr; rewrite <- Rplus_assoc;
+ fold (r - IZR (up r)) in |- *; rewrite Ropp_involutive; 
+ elim (Rplus_ne 1); intros a b; pattern 1 at 2 in |- *; 
+ rewrite <- a; clear a b; rewrite (Rplus_comm (r - IZR (up r)) 1);
+ apply Rplus_lt_compat_l; auto with zarith real.
+elim (for_base_fp r); intros; rewrite <- Ropp_0; rewrite <- Ropp_minus_distr;
+ apply Ropp_gt_lt_contravar; auto with zarith real.
 Qed.
 
 (*********************************************************)
@@ -107,446 +104,442 @@ Qed.
 (*********************************************************)
 
 (**********)
-Lemma base_Int_part:(r:R)(Rle (IZR (Int_part r)) r)/\
-                    (Rgt (Rminus (IZR (Int_part r)) r) (Ropp R1)). 
-Intro;Unfold Int_part;Elim (archimed r);Intros.
-Split;Rewrite <- (Z_R_minus (up r) `1`);Simpl.
-Generalize (Rle_minus (Rminus (IZR (up r)) r) R1 H0);Intro;
- Unfold Rminus in H1;
- Rewrite (Rplus_assoc (IZR (up r)) (Ropp r) (Ropp R1)) in 
- H1;Rewrite (Rplus_sym (Ropp r) (Ropp R1)) in H1;
- Rewrite <-(Rplus_assoc (IZR (up r)) (Ropp R1) (Ropp r)) in
- H1;Fold (Rminus (IZR (up r)) R1) in H1;
- Fold (Rminus (Rminus (IZR (up r)) R1) r) in H1;
- Apply Rminus_le;Auto with zarith real.
-Generalize (Rgt_plus_plus_r (Ropp R1) (IZR (up r)) r H);Intro;
- Rewrite (Rplus_sym (Ropp R1) (IZR (up r))) in H1;
- Generalize (Rgt_plus_plus_r (Ropp r) 
-   (Rplus (IZR (up r)) (Ropp R1)) (Rplus (Ropp R1) r) H1);
- Intro;Clear H H0 H1;
- Rewrite (Rplus_sym (Ropp r) (Rplus (IZR (up r)) (Ropp R1)))
- in H2;Fold (Rminus (IZR (up r)) R1) in H2;
- Fold (Rminus (Rminus (IZR (up r)) R1) r) in H2;
- Rewrite (Rplus_sym (Ropp r) (Rplus (Ropp R1) r)) in H2;
- Rewrite (Rplus_assoc (Ropp R1) r (Ropp r)) in H2;
- Rewrite (Rplus_Ropp_r r) in H2;Elim (Rplus_ne (Ropp R1));Intros a b;
- Rewrite a in H2;Clear a b;Auto with zarith real.  
+Lemma base_Int_part :
+ forall r:R, IZR (Int_part r) <= r /\ IZR (Int_part r) - r > -1. 
+intro; unfold Int_part in |- *; elim (archimed r); intros.
+split; rewrite <- (Z_R_minus (up r) 1); simpl in |- *.
+generalize (Rle_minus (IZR (up r) - r) 1 H0); intro; unfold Rminus in H1;
+ rewrite (Rplus_assoc (IZR (up r)) (- r) (-1)) in H1;
+ rewrite (Rplus_comm (- r) (-1)) in H1;
+ rewrite <- (Rplus_assoc (IZR (up r)) (-1) (- r)) in H1;
+ fold (IZR (up r) - 1) in H1; fold (IZR (up r) - 1 - r) in H1;
+ apply Rminus_le; auto with zarith real.
+generalize (Rplus_gt_compat_l (-1) (IZR (up r)) r H); intro;
+ rewrite (Rplus_comm (-1) (IZR (up r))) in H1;
+ generalize (Rplus_gt_compat_l (- r) (IZR (up r) + -1) (-1 + r) H1); 
+ intro; clear H H0 H1; rewrite (Rplus_comm (- r) (IZR (up r) + -1)) in H2;
+ fold (IZR (up r) - 1) in H2; fold (IZR (up r) - 1 - r) in H2;
+ rewrite (Rplus_comm (- r) (-1 + r)) in H2;
+ rewrite (Rplus_assoc (-1) r (- r)) in H2; rewrite (Rplus_opp_r r) in H2;
+ elim (Rplus_ne (-1)); intros a b; rewrite a in H2; 
+ clear a b; auto with zarith real.  
 Qed.
 
 (**********)
-Lemma Int_part_INR:(n : nat)  (Int_part (INR n)) = (inject_nat n).
-Intros n; Unfold Int_part.
-Cut (up (INR n)) = (Zplus (inject_nat n) (inject_nat (1))).
-Intros H'; Rewrite H'; Simpl; Ring.
-Apply sym_equal; Apply tech_up; Auto.
-Replace (Zplus (inject_nat n) (inject_nat (1))) with (INZ (S n)).
-Repeat Rewrite <- INR_IZR_INZ.
-Apply lt_INR; Auto.
-Rewrite Zplus_sym; Rewrite <- inj_plus; Simpl; Auto.
-Rewrite plus_IZR; Simpl; Auto with real.
-Repeat Rewrite <- INR_IZR_INZ; Auto with real.
+Lemma Int_part_INR : forall n:nat, Int_part (INR n) = Z_of_nat n.
+intros n; unfold Int_part in |- *.
+cut (up (INR n) = (Z_of_nat n + Z_of_nat 1)%Z).
+intros H'; rewrite H'; simpl in |- *; ring.
+apply sym_equal; apply tech_up; auto.
+replace (Z_of_nat n + Z_of_nat 1)%Z with (Z_of_nat (S n)).
+repeat rewrite <- INR_IZR_INZ.
+apply lt_INR; auto.
+rewrite Zplus_comm; rewrite <- Znat.inj_plus; simpl in |- *; auto.
+rewrite plus_IZR; simpl in |- *; auto with real.
+repeat rewrite <- INR_IZR_INZ; auto with real.
 Qed.
 
 (**********)
-Lemma fp_nat:(r:R)(frac_part r)==R0->(Ex [c:Z](r==(IZR c))).
-Unfold frac_part;Intros;Split with (Int_part r);Apply Rminus_eq; Auto with zarith real.
+Lemma fp_nat : forall r:R, frac_part r = 0 ->  exists c : Z | r = IZR c.
+unfold frac_part in |- *; intros; split with (Int_part r);
+ apply Rminus_diag_uniq; auto with zarith real.
 Qed.
 
 (**********)
-Lemma R0_fp_O:(r:R)~R0==(frac_part r)->~R0==r.
-Red;Intros;Rewrite <- H0 in H;Generalize fp_R0;Intro;Auto with zarith real.
+Lemma R0_fp_O : forall r:R, 0 <> frac_part r -> 0 <> r.
+red in |- *; intros; rewrite <- H0 in H; generalize fp_R0; intro;
+ auto with zarith real.
 Qed.
 
 (**********)
-Lemma Rminus_Int_part1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))->
-  (Int_part (Rminus r1 r2))=(Zminus (Int_part r1) (Int_part r2)).
-Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;
- Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0;
- Generalize (Rle_Ropp R0 (frac_part r2) H4);Intro;Clear H4;
- Rewrite (Ropp_O) in H0;
- Generalize (Rle_sym2 (Ropp (frac_part r2)) R0 H0);Intro;Clear H0;
- Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2;
- Generalize (Rlt_Ropp (frac_part r2) R1 H1);Intro;Clear H1;
- Unfold Rgt in H2;
- Generalize (sum_inequa_Rle_lt R0 (frac_part r1) R1 (Ropp R1)
-   (Ropp (frac_part r2)) R0 H0 H3 H2 H4);Intro;Elim H1;Intros;
- Clear H1;Elim (Rplus_ne R1);Intros a b;Rewrite a in H6;Clear a b H5;
- Generalize (Rge_minus (frac_part r1) (frac_part r2) H);Intro;Clear H;
- Fold (Rminus (frac_part r1) (frac_part r2)) in H6;
- Generalize (Rle_sym2 R0 (Rminus (frac_part r1) (frac_part r2)) H1);
- Intro;Clear H1 H3 H4 H0 H2;Unfold frac_part in H6 H;
- Unfold Rminus in H6 H;
- Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H;
- Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
-  (IZR (Int_part r2))) in H;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H;
- Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
-  (IZR (Int_part r2))) in H;
- Rewrite <-(Rplus_assoc r1 (Ropp r2) 
-  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H;
- Fold (Rminus r1 r2) in H;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
- in H;Generalize (Rle_compatibility 
-  (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R0 
-  (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) H);Intro;
- Clear H;Rewrite (Rplus_sym (Rminus r1 r2)
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H0;
- Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H0;
- Unfold Rminus in H0;Fold (Rminus r1 r2) in H0;
- Rewrite (Rplus_assoc (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))) 
-  (Rplus (IZR (Int_part r2)) (Ropp (IZR (Int_part r1))))) in H0;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r2))) (IZR (Int_part r2))
-  (Ropp (IZR (Int_part r1)))) in H0;Rewrite (Rplus_Ropp_l (IZR (Int_part r2))) in 
- H0;Elim (Rplus_ne (Ropp (IZR (Int_part r1))));Intros a b;Rewrite b in H0;
- Clear a b;
- Elim (Rplus_ne (Rplus (IZR (Int_part r1)) (Ropp (IZR (Int_part r2)))));
- Intros a b;Rewrite a in H0;Clear a b;Rewrite (Rplus_Ropp_r (IZR (Int_part r1))) 
- in H0;Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H0;
- Clear a b;Fold (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
- Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H6;
- Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H6;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H6;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
-  (IZR (Int_part r2))) in H6;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H6;
- Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
-  (IZR (Int_part r2))) in H6;
- Rewrite <-(Rplus_assoc r1 (Ropp r2) 
-  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H6;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H6;
- Fold (Rminus r1 r2) in H6;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
- in H6;Generalize (Rlt_compatibility 
-   (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) 
-   (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) R1 H6);
- Intro;Clear H6;
- Rewrite (Rplus_sym (Rminus r1 r2)
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H;
- Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H;
- Rewrite <-(Ropp_distr2 (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
- Rewrite (Rplus_Ropp_r (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H;
- Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H;Clear a b;
- Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
- Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
- Cut R1==(IZR `1`);Auto with zarith real.
-Intro;Rewrite H1 in H;Clear H1;
- Rewrite <-(plus_IZR `(Int_part r1)-(Int_part r2)` `1`) in H;
- Generalize (up_tech  (Rminus r1 r2) `(Int_part r1)-(Int_part r2)`
-  H0 H);Intros;Clear H H0;Unfold 1 Int_part;Omega.
+Lemma Rminus_Int_part1 :
+ forall r1 r2:R,
+   frac_part r1 >= frac_part r2 ->
+   Int_part (r1 - r2) = (Int_part r1 - Int_part r2)%Z.
+intros; elim (base_fp r1); elim (base_fp r2); intros;
+ generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0;
+ generalize (Ropp_le_ge_contravar 0 (frac_part r2) H4); 
+ intro; clear H4; rewrite Ropp_0 in H0;
+ generalize (Rge_le 0 (- frac_part r2) H0); intro; 
+ clear H0; generalize (Rge_le (frac_part r1) 0 H2); 
+ intro; clear H2; generalize (Ropp_lt_gt_contravar (frac_part r2) 1 H1);
+ intro; clear H1; unfold Rgt in H2;
+ generalize
+  (sum_inequa_Rle_lt 0 (frac_part r1) 1 (-1) (- frac_part r2) 0 H0 H3 H2 H4);
+ intro; elim H1; intros; clear H1; elim (Rplus_ne 1); 
+ intros a b; rewrite a in H6; clear a b H5;
+ generalize (Rge_minus (frac_part r1) (frac_part r2) H); 
+ intro; clear H; fold (frac_part r1 - frac_part r2) in H6;
+ generalize (Rge_le (frac_part r1 - frac_part r2) 0 H1); 
+ intro; clear H1 H3 H4 H0 H2; unfold frac_part in H6, H;
+ unfold Rminus in H6, H;
+ rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H;
+ rewrite (Ropp_involutive (IZR (Int_part r2))) in H;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
+   in H;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
+   in H; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H;
+ rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
+   in H; rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ fold (r1 - r2) in H; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H;
+ generalize
+  (Rplus_le_compat_l (IZR (Int_part r1) - IZR (Int_part r2)) 0
+     (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) H); 
+ intro; clear H;
+ rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H0;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
+     (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
+   in H0; unfold Rminus in H0; fold (r1 - r2) in H0;
+ rewrite
+  (Rplus_assoc (IZR (Int_part r1)) (- IZR (Int_part r2))
+     (IZR (Int_part r2) + - IZR (Int_part r1))) in H0;
+ rewrite <-
+  (Rplus_assoc (- IZR (Int_part r2)) (IZR (Int_part r2))
+     (- IZR (Int_part r1))) in H0;
+ rewrite (Rplus_opp_l (IZR (Int_part r2))) in H0;
+ elim (Rplus_ne (- IZR (Int_part r1))); intros a b; 
+ rewrite b in H0; clear a b;
+ elim (Rplus_ne (IZR (Int_part r1) + - IZR (Int_part r2))); 
+ intros a b; rewrite a in H0; clear a b;
+ rewrite (Rplus_opp_r (IZR (Int_part r1))) in H0; elim (Rplus_ne (r1 - r2));
+ intros a b; rewrite b in H0; clear a b;
+ fold (IZR (Int_part r1) - IZR (Int_part r2)) in H0;
+ rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H6;
+ rewrite (Ropp_involutive (IZR (Int_part r2))) in H6;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
+   in H6;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
+   in H6; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H6;
+ rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H6;
+ rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
+   in H6;
+ rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H6;
+ fold (r1 - r2) in H6; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H6;
+ generalize
+  (Rplus_lt_compat_l (IZR (Int_part r1) - IZR (Int_part r2))
+     (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) 1 H6); 
+ intro; clear H6;
+ rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
+     (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
+   in H;
+ rewrite <- (Ropp_minus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H;
+ elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; 
+ clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
+ rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; 
+ cut (1 = IZR 1); auto with zarith real.
+intro; rewrite H1 in H; clear H1;
+ rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H;
+ generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); 
+ intros; clear H H0; unfold Int_part at 1 in |- *; 
+ omega.
 Qed.
 
 (**********)
-Lemma Rminus_Int_part2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))->
-  (Int_part (Rminus r1 r2))=(Zminus (Zminus (Int_part r1) (Int_part r2)) `1`).
-Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;
- Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0;
- Generalize (Rle_Ropp R0 (frac_part r2) H4);Intro;Clear H4;
- Rewrite (Ropp_O) in H0;
- Generalize (Rle_sym2 (Ropp (frac_part r2)) R0 H0);Intro;Clear H0;
- Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2;
- Generalize (Rlt_Ropp (frac_part r2) R1 H1);Intro;Clear H1;
- Unfold Rgt in H2;
- Generalize (sum_inequa_Rle_lt R0 (frac_part r1) R1 (Ropp R1)
-   (Ropp (frac_part r2)) R0 H0 H3 H2 H4);Intro;Elim H1;Intros;
- Clear H1;Elim (Rplus_ne (Ropp R1));Intros a b;Rewrite b in H5;
- Clear a b H6;Generalize (Rlt_minus (frac_part r1) (frac_part r2) H);
- Intro;Clear H;Fold (Rminus (frac_part r1) (frac_part r2)) in H5;
- Clear H3 H4 H0 H2;Unfold frac_part in H5 H1;
- Unfold Rminus in H5 H1;
- Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H5;
- Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H5;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H5;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
-  (IZR (Int_part r2))) in H5;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H5;
- Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
-  (IZR (Int_part r2))) in H5;
- Rewrite <-(Rplus_assoc r1 (Ropp r2) 
-  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H5;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H5;
- Fold (Rminus r1 r2) in H5;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
- in H5;Generalize (Rlt_compatibility 
-  (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) (Ropp R1) 
-  (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) H5);
- Intro;Clear H5;Rewrite (Rplus_sym (Rminus r1 r2)
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H;
- Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H;
- Unfold Rminus in H;Fold (Rminus r1 r2) in H;
- Rewrite (Rplus_assoc (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))) 
-  (Rplus (IZR (Int_part r2)) (Ropp (IZR (Int_part r1))))) in H;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r2))) (IZR (Int_part r2))
-  (Ropp (IZR (Int_part r1)))) in H;Rewrite (Rplus_Ropp_l (IZR (Int_part r2))) in 
- H;Elim (Rplus_ne (Ropp (IZR (Int_part r1))));Intros a b;Rewrite b in H;
- Clear a b;Rewrite (Rplus_Ropp_r (IZR (Int_part r1))) in H;
- Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H;
- Clear a b;Fold (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
- Fold (Rminus (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R1) in H;
- Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H1;
- Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H1;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H1;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
-  (IZR (Int_part r2))) in H1;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H1;
- Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
-  (IZR (Int_part r2))) in H1;
- Rewrite <-(Rplus_assoc r1 (Ropp r2) 
-  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H1;
- Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H1;
- Fold (Rminus r1 r2) in H1;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
- in H1;Generalize (Rlt_compatibility 
-   (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) 
-   (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) R0 H1);
- Intro;Clear H1;
- Rewrite (Rplus_sym (Rminus r1 r2)
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H0;
- Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H0;
- Rewrite <-(Ropp_distr2 (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
- Rewrite (Rplus_Ropp_r (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0;
- Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H0;Clear a b;
- Rewrite <-(Rplus_Ropp_l R1) in H0;
- Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Ropp R1) R1) in H0;
- Fold (Rminus (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R1) in H0;
- Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
- Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
- Cut R1==(IZR `1`);Auto with zarith real.
-Intro;Rewrite H1 in H;Rewrite H1 in H0;Clear H1;
- Rewrite (Z_R_minus `(Int_part r1)-(Int_part r2)` `1`) in H;
- Rewrite (Z_R_minus `(Int_part r1)-(Int_part r2)` `1`) in H0;
- Rewrite <-(plus_IZR `(Int_part r1)-(Int_part r2)-1` `1`) in H0;
- Generalize (Rlt_le (IZR `(Int_part r1)-(Int_part r2)-1`) (Rminus r1 r2) H);
- Intro;Clear H;
- Generalize (up_tech  (Rminus r1 r2) `(Int_part r1)-(Int_part r2)-1`
-  H1 H0);Intros;Clear H0 H1;Unfold 1 Int_part;Omega.
+Lemma Rminus_Int_part2 :
+ forall r1 r2:R,
+   frac_part r1 < frac_part r2 ->
+   Int_part (r1 - r2) = (Int_part r1 - Int_part r2 - 1)%Z.
+intros; elim (base_fp r1); elim (base_fp r2); intros;
+ generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0;
+ generalize (Ropp_le_ge_contravar 0 (frac_part r2) H4); 
+ intro; clear H4; rewrite Ropp_0 in H0;
+ generalize (Rge_le 0 (- frac_part r2) H0); intro; 
+ clear H0; generalize (Rge_le (frac_part r1) 0 H2); 
+ intro; clear H2; generalize (Ropp_lt_gt_contravar (frac_part r2) 1 H1);
+ intro; clear H1; unfold Rgt in H2;
+ generalize
+  (sum_inequa_Rle_lt 0 (frac_part r1) 1 (-1) (- frac_part r2) 0 H0 H3 H2 H4);
+ intro; elim H1; intros; clear H1; elim (Rplus_ne (-1)); 
+ intros a b; rewrite b in H5; clear a b H6;
+ generalize (Rlt_minus (frac_part r1) (frac_part r2) H); 
+ intro; clear H; fold (frac_part r1 - frac_part r2) in H5; 
+ clear H3 H4 H0 H2; unfold frac_part in H5, H1; unfold Rminus in H5, H1;
+ rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H5;
+ rewrite (Ropp_involutive (IZR (Int_part r2))) in H5;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
+   in H5;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
+   in H5; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H5;
+ rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H5;
+ rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
+   in H5;
+ rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H5;
+ fold (r1 - r2) in H5; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H5;
+ generalize
+  (Rplus_lt_compat_l (IZR (Int_part r1) - IZR (Int_part r2)) (-1)
+     (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) H5); 
+ intro; clear H5;
+ rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
+     (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
+   in H; unfold Rminus in H; fold (r1 - r2) in H;
+ rewrite
+  (Rplus_assoc (IZR (Int_part r1)) (- IZR (Int_part r2))
+     (IZR (Int_part r2) + - IZR (Int_part r1))) in H;
+ rewrite <-
+  (Rplus_assoc (- IZR (Int_part r2)) (IZR (Int_part r2))
+     (- IZR (Int_part r1))) in H;
+ rewrite (Rplus_opp_l (IZR (Int_part r2))) in H;
+ elim (Rplus_ne (- IZR (Int_part r1))); intros a b; 
+ rewrite b in H; clear a b; rewrite (Rplus_opp_r (IZR (Int_part r1))) in H;
+ elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; 
+ clear a b; fold (IZR (Int_part r1) - IZR (Int_part r2)) in H;
+ fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H;
+ rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2))) in H1;
+ rewrite (Ropp_involutive (IZR (Int_part r2))) in H1;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)))
+   in H1;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)))
+   in H1; rewrite (Rplus_comm (- IZR (Int_part r1)) (- r2)) in H1;
+ rewrite (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
+ rewrite <- (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)))
+   in H1;
+ rewrite (Rplus_comm (- IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
+ fold (r1 - r2) in H1; fold (IZR (Int_part r2) - IZR (Int_part r1)) in H1;
+ generalize
+  (Rplus_lt_compat_l (IZR (Int_part r1) - IZR (Int_part r2))
+     (r1 - r2 + (IZR (Int_part r2) - IZR (Int_part r1))) 0 H1); 
+ intro; clear H1;
+ rewrite (Rplus_comm (r1 - r2) (IZR (Int_part r2) - IZR (Int_part r1))) in H0;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2))
+     (IZR (Int_part r2) - IZR (Int_part r1)) (r1 - r2))
+   in H0;
+ rewrite <- (Ropp_minus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
+ rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H0;
+ elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H0; 
+ clear a b; rewrite <- (Rplus_opp_l 1) in H0;
+ rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-1) 1)
+   in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0;
+ rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
+ rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; 
+ cut (1 = IZR 1); auto with zarith real.
+intro; rewrite H1 in H; rewrite H1 in H0; clear H1;
+ rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H;
+ rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0;
+ rewrite <- (plus_IZR (Int_part r1 - Int_part r2 - 1) 1) in H0;
+ generalize (Rlt_le (IZR (Int_part r1 - Int_part r2 - 1)) (r1 - r2) H); 
+ intro; clear H;
+ generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0); 
+ intros; clear H0 H1; unfold Int_part at 1 in |- *; 
+ omega.
 Qed.
 
 (**********)
-Lemma Rminus_fp1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))->
-  (frac_part (Rminus r1 r2))==(Rminus (frac_part r1) (frac_part r2)).
-Intros;Unfold frac_part;
- Generalize (Rminus_Int_part1 r1 r2 H);Intro;Rewrite -> H0;
- Rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));Unfold Rminus;
- Rewrite -> (Ropp_distr1 (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))));
- Rewrite -> (Ropp_distr1 r2 (Ropp (IZR (Int_part r2))));
- Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));
- Rewrite -> (Rplus_assoc r1 (Ropp r2)
-             (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))));
- Rewrite -> (Rplus_assoc r1 (Ropp (IZR (Int_part r1)))
-             (Rplus (Ropp r2) (IZR (Int_part r2))));
- Rewrite <- (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
-             (IZR (Int_part r2)));
- Rewrite <- (Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
-             (IZR (Int_part r2)));
- Rewrite -> (Rplus_sym (Ropp r2) (Ropp (IZR (Int_part r1))));Auto with zarith real.
+Lemma Rminus_fp1 :
+ forall r1 r2:R,
+   frac_part r1 >= frac_part r2 ->
+   frac_part (r1 - r2) = frac_part r1 - frac_part r2.
+intros; unfold frac_part in |- *; generalize (Rminus_Int_part1 r1 r2 H);
+ intro; rewrite H0; rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));
+ unfold Rminus in |- *;
+ rewrite (Ropp_plus_distr (IZR (Int_part r1)) (- IZR (Int_part r2)));
+ rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2)));
+ rewrite (Ropp_involutive (IZR (Int_part r2)));
+ rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)));
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)));
+ rewrite <- (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2)));
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)));
+ rewrite (Rplus_comm (- r2) (- IZR (Int_part r1))); 
+ auto with zarith real.
 Qed.
 
 (**********)
-Lemma Rminus_fp2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))->
-  (frac_part (Rminus r1 r2))==
-  (Rplus (Rminus (frac_part r1) (frac_part r2)) R1).
-Intros;Unfold frac_part;Generalize (Rminus_Int_part2 r1 r2 H);Intro;
- Rewrite -> H0;
- Rewrite <- (Z_R_minus (Zminus (Int_part r1) (Int_part r2)) `1`);
- Rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));Unfold Rminus;
- Rewrite -> (Ropp_distr1 (Rplus (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))))
-             (Ropp (IZR `1`)));
- Rewrite -> (Ropp_distr1 r2 (Ropp (IZR (Int_part r2))));
- Rewrite -> (Ropp_Ropp (IZR `1`));
- Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));
- Rewrite -> (Ropp_distr1 (IZR (Int_part r1)));
- Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));Simpl;
- Rewrite <- (Rplus_assoc (Rplus r1 (Ropp r2))
-             (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) R1);
- Rewrite -> (Rplus_assoc r1 (Ropp r2)
-             (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))));
- Rewrite -> (Rplus_assoc r1 (Ropp (IZR (Int_part r1)))
-             (Rplus (Ropp r2) (IZR (Int_part r2)))); 
- Rewrite <- (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
-             (IZR (Int_part r2)));
- Rewrite <- (Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
-             (IZR (Int_part r2)));
- Rewrite -> (Rplus_sym (Ropp r2) (Ropp (IZR (Int_part r1))));Auto with zarith real.
+Lemma Rminus_fp2 :
+ forall r1 r2:R,
+   frac_part r1 < frac_part r2 ->
+   frac_part (r1 - r2) = frac_part r1 - frac_part r2 + 1.
+intros; unfold frac_part in |- *; generalize (Rminus_Int_part2 r1 r2 H);
+ intro; rewrite H0; rewrite <- (Z_R_minus (Int_part r1 - Int_part r2) 1);
+ rewrite <- (Z_R_minus (Int_part r1) (Int_part r2)); 
+ unfold Rminus in |- *;
+ rewrite
+  (Ropp_plus_distr (IZR (Int_part r1) + - IZR (Int_part r2)) (- IZR 1))
+  ; rewrite (Ropp_plus_distr r2 (- IZR (Int_part r2)));
+ rewrite (Ropp_involutive (IZR 1));
+ rewrite (Ropp_involutive (IZR (Int_part r2)));
+ rewrite (Ropp_plus_distr (IZR (Int_part r1)));
+ rewrite (Ropp_involutive (IZR (Int_part r2))); simpl in |- *;
+ rewrite <-
+  (Rplus_assoc (r1 + - r2) (- IZR (Int_part r1) + IZR (Int_part r2)) 1)
+  ; rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)));
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (- r2 + IZR (Int_part r2)));
+ rewrite <- (Rplus_assoc (- r2) (- IZR (Int_part r1)) (IZR (Int_part r2)));
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- r2) (IZR (Int_part r2)));
+ rewrite (Rplus_comm (- r2) (- IZR (Int_part r1))); 
+ auto with zarith real.
 Qed.
 
 (**********)
-Lemma plus_Int_part1:(r1,r2:R)(Rge (Rplus (frac_part r1) (frac_part r2)) R1)->
-  (Int_part (Rplus r1 r2))=(Zplus (Zplus (Int_part r1) (Int_part r2)) `1`).
-Intros;
- Generalize (Rle_sym2 R1 (Rplus (frac_part r1) (frac_part r2)) H);
- Intro;Clear H;Elim (base_fp r1);Elim (base_fp r2);Intros;Clear H H2;
- Generalize (Rlt_compatibility (frac_part r2) (frac_part r1) R1 H3);
- Intro;Clear H3;
- Generalize (Rlt_compatibility R1 (frac_part r2) R1 H1);Intro;Clear H1;
- Rewrite (Rplus_sym R1 (frac_part r2)) in H2;
- Generalize (Rlt_trans (Rplus (frac_part r2) (frac_part r1))
-  (Rplus (frac_part r2) R1) (Rplus R1 R1) H H2);Intro;Clear H H2;
- Rewrite (Rplus_sym (frac_part r2) (frac_part r1)) in H1;
- Unfold frac_part in H0 H1;Unfold Rminus in H0 H1;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H1;
- Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H1;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
-  r2) in H1;
- Rewrite (Rplus_sym 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H1;
- Rewrite <-(Rplus_assoc r1 r2 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H1;
- Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H0;
- Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H0;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
-  r2) in H0;
- Rewrite (Rplus_sym 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H0;
- Rewrite <-(Rplus_assoc r1 r2 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H0;
- Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
- Generalize (Rle_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  R1 (Rplus (Rplus r1 r2)
-           (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) H0);Intro;
- Clear H0;
- Generalize (Rlt_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Rplus (Rplus r1 r2)
-   (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) (Rplus R1 R1) H1);
- Intro;Clear H1;
- Rewrite (Rplus_sym (Rplus r1 r2) 
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H;
- Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H;
- Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H;
- Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H;Clear a b;
- Rewrite (Rplus_sym (Rplus r1 r2) 
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H0;
- Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H0;
- Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0;
- Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H0;Clear a b;
- Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1 R1) in 
- H0;Cut R1==(IZR `1`);Auto with zarith real.
-Intro;Rewrite H1 in H0;Rewrite H1 in H;Clear H1;
- Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H; 
- Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H0;
- Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H;
- Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H0;
- Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)+1` `1`) in H0;
- Generalize (up_tech (Rplus r1 r2) `(Int_part r1)+(Int_part r2)+1` H H0);Intro;
- Clear H H0;Unfold 1 Int_part;Omega.
+Lemma plus_Int_part1 :
+ forall r1 r2:R,
+   frac_part r1 + frac_part r2 >= 1 ->
+   Int_part (r1 + r2) = (Int_part r1 + Int_part r2 + 1)%Z.
+intros; generalize (Rge_le (frac_part r1 + frac_part r2) 1 H); intro; clear H;
+ elim (base_fp r1); elim (base_fp r2); intros; clear H H2;
+ generalize (Rplus_lt_compat_l (frac_part r2) (frac_part r1) 1 H3); 
+ intro; clear H3; generalize (Rplus_lt_compat_l 1 (frac_part r2) 1 H1); 
+ intro; clear H1; rewrite (Rplus_comm 1 (frac_part r2)) in H2;
+ generalize
+  (Rlt_trans (frac_part r2 + frac_part r1) (frac_part r2 + 1) 2 H H2); 
+ intro; clear H H2; rewrite (Rplus_comm (frac_part r2) (frac_part r1)) in H1;
+ unfold frac_part in H0, H1; unfold Rminus in H0, H1;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
+   in H1; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H1;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2)
+   in H1;
+ rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H1;
+ rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
+   in H1;
+ rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
+   in H0; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H0;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2)
+   in H0;
+ rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H0;
+ rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
+   in H0;
+ rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
+ generalize
+  (Rplus_le_compat_l (IZR (Int_part r1) + IZR (Int_part r2)) 1
+     (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) H0); 
+ intro; clear H0;
+ generalize
+  (Rplus_lt_compat_l (IZR (Int_part r1) + IZR (Int_part r2))
+     (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) 2 H1); 
+ intro; clear H1;
+ rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
+   in H;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
+     (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
+   in H; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H;
+ elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H; 
+ clear a b;
+ rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
+   in H0;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
+     (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
+   in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0;
+ elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0; 
+ clear a b;
+ rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0;
+ cut (1 = IZR 1); auto with zarith real.
+intro; rewrite H1 in H0; rewrite H1 in H; clear H1;
+ rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H;
+ rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
+ rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H;
+ rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0;
+ rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0;
+ generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); 
+ intro; clear H H0; unfold Int_part at 1 in |- *; omega.
 Qed.
 
 (**********)
-Lemma plus_Int_part2:(r1,r2:R)(Rlt (Rplus (frac_part r1) (frac_part r2)) R1)->
-  (Int_part (Rplus r1 r2))=(Zplus (Int_part r1) (Int_part r2)).
-Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;Clear H1 H3;
- Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0;
- Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2;
- Generalize (Rle_compatibility (frac_part r1) R0 (frac_part r2) H1);
- Intro;Clear H1;Elim (Rplus_ne (frac_part r1));Intros a b;
- Rewrite a in H2;Clear a b;Generalize (Rle_trans R0 (frac_part r1)
-  (Rplus (frac_part r1) (frac_part r2)) H0 H2);Intro;Clear H0 H2;
- Unfold frac_part in H H1;Unfold Rminus in H H1;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H1;
- Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H1;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
-  r2) in H1;
- Rewrite (Rplus_sym 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H1;
- Rewrite <-(Rplus_assoc r1 r2 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H1;
- Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H;
- Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H;
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
-  r2) in H;
- Rewrite (Rplus_sym 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H;
- Rewrite <-(Rplus_assoc r1 r2 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H;
- Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
- Generalize (Rle_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  R0 (Rplus (Rplus r1 r2)
-           (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) H1);Intro;
- Clear H1;
- Generalize (Rlt_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Rplus (Rplus r1 r2)
-   (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) R1 H);
- Intro;Clear H;
- Rewrite (Rplus_sym (Rplus r1 r2) 
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H1;
- Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H1;
- Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H1;
- Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H1;Clear a b;
- Rewrite (Rplus_sym (Rplus r1 r2) 
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H0;
- Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H0;
- Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0;
- Elim (Rplus_ne (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))));Intros a b;
- Rewrite a in H0;Clear a b;Elim (Rplus_ne (Rplus r1 r2));Intros a b;
- Rewrite b in H0;Clear a b;Cut R1==(IZR `1`);Auto with zarith real.
-Intro;Rewrite H in H1;Clear H;
- Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H0;
- Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H1;
- Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H1;
- Generalize (up_tech (Rplus r1 r2) `(Int_part r1)+(Int_part r2)` H0 H1);Intro;
- Clear H0 H1;Unfold 1 Int_part;Omega.
+Lemma plus_Int_part2 :
+ forall r1 r2:R,
+   frac_part r1 + frac_part r2 < 1 ->
+   Int_part (r1 + r2) = (Int_part r1 + Int_part r2)%Z.
+intros; elim (base_fp r1); elim (base_fp r2); intros; clear H1 H3;
+ generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0;
+ generalize (Rge_le (frac_part r1) 0 H2); intro; clear H2;
+ generalize (Rplus_le_compat_l (frac_part r1) 0 (frac_part r2) H1); 
+ intro; clear H1; elim (Rplus_ne (frac_part r1)); intros a b; 
+ rewrite a in H2; clear a b;
+ generalize (Rle_trans 0 (frac_part r1) (frac_part r1 + frac_part r2) H0 H2);
+ intro; clear H0 H2; unfold frac_part in H, H1; unfold Rminus in H, H1;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
+   in H1; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H1;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2)
+   in H1;
+ rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H1;
+ rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
+   in H1;
+ rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)))
+   in H; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H;
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2) in H;
+ rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H;
+ rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)))
+   in H;
+ rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ generalize
+  (Rplus_le_compat_l (IZR (Int_part r1) + IZR (Int_part r2)) 0
+     (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) H1); 
+ intro; clear H1;
+ generalize
+  (Rplus_lt_compat_l (IZR (Int_part r1) + IZR (Int_part r2))
+     (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) 1 H); 
+ intro; clear H;
+ rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
+   in H1;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
+     (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
+   in H1; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H1;
+ elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H1; 
+ clear a b;
+ rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))))
+   in H0;
+ rewrite <-
+  (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2))
+     (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2))
+   in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0;
+ elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); 
+ intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2));
+ intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1);
+ auto with zarith real.
+intro; rewrite H in H1; clear H;
+ rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
+ rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1;
+ rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1;
+ generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); 
+ intro; clear H0 H1; unfold Int_part at 1 in |- *; 
+ omega.
 Qed.
 
 (**********)
-Lemma plus_frac_part1:(r1,r2:R)
-  (Rge (Rplus (frac_part r1) (frac_part r2)) R1)->
-                (frac_part (Rplus r1 r2))==
-                (Rminus (Rplus (frac_part r1) (frac_part r2)) R1).
-Intros;Unfold frac_part;
- Generalize (plus_Int_part1 r1 r2 H);Intro;Rewrite H0;
- Rewrite (plus_IZR `(Int_part r1)+(Int_part r2)` `1`);
- Rewrite (plus_IZR (Int_part r1) (Int_part r2));Simpl;Unfold 3 4 Rminus;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus r2 (Ropp (IZR (Int_part r2)))));
- Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2))));
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
-   r2);
- Rewrite (Rplus_sym 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2);
- Rewrite <-(Rplus_assoc r1 r2 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))));
- Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2)));
- Unfold Rminus;
- Rewrite (Rplus_assoc (Rplus r1 r2) 
-  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))
-  (Ropp R1));
- Rewrite <-(Ropp_distr1 (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1);
- Trivial with zarith real.
+Lemma plus_frac_part1 :
+ forall r1 r2:R,
+   frac_part r1 + frac_part r2 >= 1 ->
+   frac_part (r1 + r2) = frac_part r1 + frac_part r2 - 1.
+intros; unfold frac_part in |- *; generalize (plus_Int_part1 r1 r2 H); intro;
+ rewrite H0; rewrite (plus_IZR (Int_part r1 + Int_part r2) 1);
+ rewrite (plus_IZR (Int_part r1) (Int_part r2)); simpl in |- *;
+ unfold Rminus at 3 4 in |- *;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)));
+ rewrite (Rplus_comm r2 (- IZR (Int_part r2)));
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2);
+ rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2);
+ rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)));
+ rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2)));
+ unfold Rminus in |- *;
+ rewrite
+  (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-1))
+  ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1);
+ trivial with zarith real.
 Qed.
 
 (**********)
-Lemma plus_frac_part2:(r1,r2:R)
-  (Rlt (Rplus (frac_part r1) (frac_part r2)) R1)->
-(frac_part (Rplus r1 r2))==(Rplus (frac_part r1) (frac_part r2)).
-Intros;Unfold frac_part;
- Generalize (plus_Int_part2 r1 r2 H);Intro;Rewrite H0;
- Rewrite (plus_IZR (Int_part r1) (Int_part r2));Unfold 2 3 Rminus;
- Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
-  (Rplus r2 (Ropp (IZR (Int_part r2)))));
- Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2))));
- Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
-  r2);
- Rewrite (Rplus_sym 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2);
- Rewrite <-(Rplus_assoc r1 r2 
-  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))));
- Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2)));Unfold Rminus;
- Trivial with zarith real.
-Qed.
+Lemma plus_frac_part2 :
+ forall r1 r2:R,
+   frac_part r1 + frac_part r2 < 1 ->
+   frac_part (r1 + r2) = frac_part r1 + frac_part r2.
+intros; unfold frac_part in |- *; generalize (plus_Int_part2 r1 r2 H); intro;
+ rewrite H0; rewrite (plus_IZR (Int_part r1) (Int_part r2));
+ unfold Rminus at 2 3 in |- *;
+ rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2)));
+ rewrite (Rplus_comm r2 (- IZR (Int_part r2)));
+ rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2);
+ rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2);
+ rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)));
+ rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2)));
+ unfold Rminus in |- *; trivial with zarith real.
+Qed.
\ No newline at end of file