aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Sqrt_reg.v
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2013-12-03 16:43:14 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2013-12-03 16:43:14 +0100
commit943133d5a47ce4663a9b77a03b36c7c87c78d886 (patch)
tree6321ab6fab78b5fb723310096be3eaba9ce753a1 /theories/Reals/Sqrt_reg.v
parentaca9c227772e3765833605866ac413e61a98d04a (diff)
Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.
Diffstat (limited to 'theories/Reals/Sqrt_reg.v')
-rw-r--r--theories/Reals/Sqrt_reg.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 89c178213..985faa21e 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -32,7 +32,7 @@ Proof.
apply H0.
pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
- apply Rplus_lt_reg_r with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
+ apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r.
pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
@@ -43,7 +43,7 @@ Proof.
assumption.
apply H0.
left; apply Rlt_0_1.
- apply Rplus_lt_reg_r with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
+ apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r.
pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
@@ -75,7 +75,7 @@ Proof.
assumption.
left; apply Rlt_0_1.
apply H0.
- apply Rle_ge; left; apply Rplus_lt_reg_r with 1.
+ apply Rle_ge; left; apply Rplus_lt_reg_l with 1.
rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus;
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1.