diff options
| author | JPR | 2019-05-23 23:44:32 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:44:32 +0200 |
| commit | ab2ce9241e989ac899e4d43333b527e124c0c749 (patch) | |
| tree | 60ff7a9d9530b47a1bcff8db86b87b04fe6e7846 /theories | |
| parent | d306f5428db0d034aea55d3f0699c67c1f296cc1 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/RIneq.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index c41ab905e0..45cd74cf48 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -95,7 +95,7 @@ Proof. Qed. (*********************************************************) -(** ** Relating [<], [>], [<=] and [>=] *) +(** ** Relating [<], [>], [<=] and [>=] *) (*********************************************************) (*********************************************************) @@ -711,7 +711,7 @@ Proof. Qed. (*********************************************************) -(** ** Subtraction *) +(** ** Subtraction *) (*********************************************************) Lemma Rminus_0_r : forall r, r - 0 = r. @@ -1352,7 +1352,7 @@ Proof. Qed. (*********************************************************) -(** ** Order and subtraction *) +(** ** Order and subtraction *) (*********************************************************) Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. |