summaryrefslogtreecommitdiff
path: root/theories/Reals/R_Ifp.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/R_Ifp.v')
-rw-r--r--theories/Reals/R_Ifp.v126
1 files changed, 63 insertions, 63 deletions
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 82d7bebd..57b2c767 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: R_Ifp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
(**********************************************************)
(** Complements for the reals.Integer and fractional part *)
@@ -32,10 +32,10 @@ Lemma tech_up : forall (r:R) (z:Z), r < IZR z -> IZR z <= r + 1 -> z = up r.
Proof.
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);
+ 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)));
+ 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.
@@ -56,15 +56,15 @@ Qed.
Lemma fp_R0 : frac_part 0 = 0.
Proof.
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;
+ 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.
+ 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 H1; generalize (le_IZR_R1 (up 0) H0);
intro; clear H H0; omega.
Qed.
@@ -92,12 +92,12 @@ Proof.
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*)
+ (*inf a 1*)
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 |- *;
+ 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;
@@ -110,7 +110,7 @@ Qed.
(**********)
Lemma base_Int_part :
- forall r:R, IZR (Int_part r) <= r /\ IZR (Int_part r) - r > -1.
+ forall r:R, IZR (Int_part r) <= r /\ IZR (Int_part r) - r > -1.
Proof.
intro; unfold Int_part in |- *; elim (archimed r); intros.
split; rewrite <- (Z_R_minus (up r) 1); simpl in |- *.
@@ -122,13 +122,13 @@ Proof.
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);
+ 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.
+ elim (Rplus_ne (-1)); intros a b; rewrite a in H2;
+ clear a b; auto with zarith real.
Qed.
(**********)
@@ -168,19 +168,19 @@ Lemma Rminus_Int_part1 :
Proof.
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);
+ 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);
+ 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);
+ 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);
+ 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);
+ 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;
@@ -195,7 +195,7 @@ Proof.
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);
+ (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 <-
@@ -209,9 +209,9 @@ Proof.
(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;
+ 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)));
+ 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;
@@ -229,7 +229,7 @@ Proof.
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);
+ (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 <-
@@ -238,14 +238,14 @@ Proof.
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;
+ 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;
+ 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 |- *;
+ 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.
@@ -257,18 +257,18 @@ Lemma Rminus_Int_part2 :
Proof.
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);
+ 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);
+ 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));
+ 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;
+ 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;
@@ -283,7 +283,7 @@ Proof.
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);
+ (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 <-
@@ -297,9 +297,9 @@ Proof.
(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;
+ 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;
+ 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;
@@ -315,7 +315,7 @@ Proof.
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);
+ (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 <-
@@ -324,21 +324,21 @@ Proof.
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;
+ 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;
+ 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);
+ 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 |- *;
+ 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.
@@ -358,7 +358,7 @@ Proof.
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)));
+ rewrite (Rplus_comm (- r2) (- IZR (Int_part r1)));
auto with zarith real.
Qed.
@@ -370,7 +370,7 @@ Lemma Rminus_fp2 :
Proof.
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));
+ 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))
@@ -385,7 +385,7 @@ Proof.
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)));
+ rewrite (Rplus_comm (- r2) (- IZR (Int_part r1)));
auto with zarith real.
Qed.
@@ -397,11 +397,11 @@ Lemma plus_Int_part1 :
Proof.
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);
+ 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);
+ (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)))
@@ -422,11 +422,11 @@ Proof.
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);
+ (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);
+ (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;
@@ -434,7 +434,7 @@ Proof.
(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;
+ 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;
@@ -442,7 +442,7 @@ Proof.
(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;
+ 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.
@@ -452,7 +452,7 @@ Proof.
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);
+ 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.
@@ -465,8 +465,8 @@ Proof.
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;
+ 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;
@@ -487,11 +487,11 @@ Proof.
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);
+ (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);
+ (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;
@@ -499,7 +499,7 @@ Proof.
(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;
+ 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;
@@ -507,7 +507,7 @@ Proof.
(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)));
+ 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.
@@ -515,8 +515,8 @@ Proof.
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 |- *;
+ 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:42:36 +0000