Library Coq.Reals.RIneq
Basic lemmas for the classical real numbers
Relation between orders and equality
Reflexivity of the large order
Lemma Rle_refl :
forall r,
r <= r.
#[
global]
Hint Immediate Rle_refl:
rorders.
Lemma Rge_refl :
forall r,
r <= r.
#[
global]
Hint Immediate Rge_refl:
rorders.
Irreflexivity of the strict order
Reasoning by case on equality and order
Relating <, >, <= and >=
Order
Relating strict and large orders
Lemma Rlt_le :
forall r1 r2,
r1 < r2 -> r1 <= r2.
#[
global]
Hint Resolve Rlt_le:
real.
Lemma Rgt_ge :
forall r1 r2,
r1 > r2 -> r1 >= r2.
Lemma Rle_ge :
forall r1 r2,
r1 <= r2 -> r2 >= r1.
#[
global]
Hint Immediate Rle_ge:
real.
#[
global]
Hint Resolve Rle_ge:
rorders.
Lemma Rge_le :
forall r1 r2,
r1 >= r2 -> r2 <= r1.
#[
global]
Hint Resolve Rge_le:
real.
#[
global]
Hint Immediate Rge_le:
rorders.
Lemma Rlt_gt :
forall r1 r2,
r1 < r2 -> r2 > r1.
#[
global]
Hint Resolve Rlt_gt:
rorders.
Lemma Rgt_lt :
forall r1 r2,
r1 > r2 -> r2 < r1.
#[
global]
Hint Immediate Rgt_lt:
rorders.
Lemma Rnot_le_lt :
forall r1 r2,
~ r1 <= r2 -> r2 < r1.
#[
global]
Hint Immediate Rnot_le_lt:
real.
Lemma Rnot_ge_gt :
forall r1 r2,
~ r1 >= r2 -> r2 > r1.
Lemma Rnot_le_gt :
forall r1 r2,
~ r1 <= r2 -> r1 > r2.
Lemma Rnot_ge_lt :
forall r1 r2,
~ r1 >= r2 -> r1 < r2.
Lemma Rnot_lt_le :
forall r1 r2,
~ r1 < r2 -> r2 <= r1.
Lemma Rnot_gt_le :
forall r1 r2,
~ r1 > r2 -> r1 <= r2.
Lemma Rnot_gt_ge :
forall r1 r2,
~ r1 > r2 -> r2 >= r1.
Lemma Rnot_lt_ge :
forall r1 r2,
~ r1 < r2 -> r1 >= r2.
Lemma Rlt_not_le :
forall r1 r2,
r2 < r1 -> ~ r1 <= r2.
#[
global]
Hint Immediate Rlt_not_le:
real.
Lemma Rgt_not_le :
forall r1 r2,
r1 > r2 -> ~ r1 <= r2.
Lemma Rlt_not_ge :
forall r1 r2,
r1 < r2 -> ~ r1 >= r2.
#[
global]
Hint Immediate Rlt_not_ge:
real.
Lemma Rgt_not_ge :
forall r1 r2,
r2 > r1 -> ~ r1 >= r2.
Lemma Rle_not_lt :
forall r1 r2,
r2 <= r1 -> ~ r1 < r2.
Lemma Rge_not_lt :
forall r1 r2,
r1 >= r2 -> ~ r1 < r2.
Lemma Rle_not_gt :
forall r1 r2,
r1 <= r2 -> ~ r1 > r2.
Lemma Rge_not_gt :
forall r1 r2,
r2 >= r1 -> ~ r1 > r2.
Lemma Req_le :
forall r1 r2,
r1 = r2 -> r1 <= r2.
#[
global]
Hint Immediate Req_le:
real.
Lemma Req_ge :
forall r1 r2,
r1 = r2 -> r1 >= r2.
#[
global]
Hint Immediate Req_ge:
real.
Lemma Req_le_sym :
forall r1 r2,
r2 = r1 -> r1 <= r2.
#[
global]
Hint Immediate Req_le_sym:
real.
Lemma Req_ge_sym :
forall r1 r2,
r2 = r1 -> r1 >= r2.
#[
global]
Hint Immediate Req_ge_sym:
real.
Asymmetry
Remark:
Rlt_asym is an axiom
Compatibility with equality
Transitivity
Remark:
Rlt_trans is an axiom
Lemma Rlt_dec :
forall r1 r2,
{r1 < r2} + {~ r1 < r2}.
Lemma Rle_dec :
forall r1 r2,
{r1 <= r2} + {~ r1 <= r2}.
Lemma Rgt_dec :
forall r1 r2,
{r1 > r2} + {~ r1 > r2}.
Lemma Rge_dec :
forall r1 r2,
{r1 >= r2} + {~ r1 >= r2}.
Lemma Rlt_le_dec :
forall r1 r2,
{r1 < r2} + {r2 <= r1}.
Lemma Rgt_ge_dec :
forall r1 r2,
{r1 > r2} + {r2 >= r1}.
Lemma Rle_lt_dec :
forall r1 r2,
{r1 <= r2} + {r2 < r1}.
Lemma Rge_gt_dec :
forall r1 r2,
{r1 >= r2} + {r2 > r1}.
Lemma Rlt_or_le :
forall r1 r2,
r1 < r2 \/ r2 <= r1.
Lemma Rgt_or_ge :
forall r1 r2,
r1 > r2 \/ r2 >= r1.
Lemma Rle_or_lt :
forall r1 r2,
r1 <= r2 \/ r2 < r1.
Lemma Rge_or_gt :
forall r1 r2,
r1 >= r2 \/ r2 > r1.
Lemma Rle_lt_or_eq_dec :
forall r1 r2,
r1 <= r2 -> {r1 < r2} + {r1 = r2}.
Lemma inser_trans_R :
forall r1 r2 r3 r4,
r1 <= r2 < r3 -> {r1 <= r2 < r4} + {r4 <= r2 < r3}.
Addition
Remark:
Rplus_0_l is an axiom
Lemma Rplus_0_r :
forall r,
r + 0
= r.
#[
global]
Hint Resolve Rplus_0_r:
real.
Lemma Rplus_ne :
forall r,
r + 0
= r /\ 0
+ r = r.
#[
global]
Hint Resolve Rplus_ne:
real.
Remark: Rplus_opp_r is an axiom
Lemma Rinv_r :
forall r,
r <> 0
-> r * / r = 1.
#[
global]
Hint Resolve Rinv_r:
real.
Lemma Rinv_l_sym :
forall r,
r <> 0
-> 1
= / r * r.
#[
global]
Hint Resolve Rinv_l_sym:
real.
Lemma Rinv_r_sym :
forall r,
r <> 0
-> 1
= r * / r.
#[
global]
Hint Resolve Rinv_r_sym:
real.
Lemma Rmult_0_r :
forall r,
r * 0
= 0.
#[
global]
Hint Resolve Rmult_0_r:
real.
Lemma Rmult_0_l :
forall r, 0
* r = 0.
#[
global]
Hint Resolve Rmult_0_l:
real.
Lemma Rmult_ne :
forall r,
r * 1
= r /\ 1
* r = r.
#[
global]
Hint Resolve Rmult_ne:
real.
Lemma Rmult_1_r :
forall r,
r * 1
= r.
#[
global]
Hint Resolve Rmult_1_r:
real.
Lemma Rmult_eq_compat_l :
forall r r1 r2,
r1 = r2 -> r * r1 = r * r2.
Lemma Rmult_eq_compat_r :
forall r r1 r2,
r1 = r2 -> r1 * r = r2 * r.
Lemma Rmult_eq_reg_l :
forall r r1 r2,
r * r1 = r * r2 -> r <> 0
-> r1 = r2.
Lemma Rmult_eq_reg_r :
forall r r1 r2,
r1 * r = r2 * r -> r <> 0
-> r1 = r2.
Lemma Rmult_integral :
forall r1 r2,
r1 * r2 = 0
-> r1 = 0
\/ r2 = 0.
Lemma Rmult_eq_0_compat :
forall r1 r2,
r1 = 0
\/ r2 = 0
-> r1 * r2 = 0.
#[
global]
Hint Resolve Rmult_eq_0_compat:
real.
Lemma Rmult_eq_0_compat_r :
forall r1 r2,
r1 = 0
-> r1 * r2 = 0.
Lemma Rmult_eq_0_compat_l :
forall r1 r2,
r2 = 0
-> r1 * r2 = 0.
Lemma Rmult_neq_0_reg :
forall r1 r2,
r1 * r2 <> 0
-> r1 <> 0
/\ r2 <> 0.
Lemma Rmult_integral_contrapositive :
forall r1 r2,
r1 <> 0
/\ r2 <> 0
-> r1 * r2 <> 0.
#[
global]
Hint Resolve Rmult_integral_contrapositive:
real.
Lemma Rmult_integral_contrapositive_currified :
forall r1 r2,
r1 <> 0
-> r2 <> 0
-> r1 * r2 <> 0.
Lemma Rmult_plus_distr_r :
forall r1 r2 r3,
(r1 + r2) * r3 = r1 * r3 + r2 * r3.
Opposite and multiplication
Lemma Rminus_0_r :
forall r,
r - 0
= r.
#[
global]
Hint Resolve Rminus_0_r:
real.
Lemma Rminus_0_l :
forall r, 0
- r = - r.
#[
global]
Hint Resolve Rminus_0_l:
real.
Lemma Ropp_minus_distr :
forall r1 r2,
- (r1 - r2) = r2 - r1.
#[
global]
Hint Resolve Ropp_minus_distr:
real.
Lemma Ropp_minus_distr' :
forall r1 r2,
- (r2 - r1) = r1 - r2.
Lemma Rminus_diag_eq :
forall r1 r2,
r1 = r2 -> r1 - r2 = 0.
#[
global]
Hint Resolve Rminus_diag_eq:
real.
Lemma Rminus_eq_0 x :
x - x = 0.
Lemma Rminus_diag_uniq :
forall r1 r2,
r1 - r2 = 0
-> r1 = r2.
#[
global]
Hint Immediate Rminus_diag_uniq:
real.
Lemma Rminus_diag_uniq_sym :
forall r1 r2,
r2 - r1 = 0
-> r1 = r2.
#[
global]
Hint Immediate Rminus_diag_uniq_sym:
real.
Lemma Rplus_minus :
forall r1 r2,
r1 + (r2 - r1) = r2.
#[
global]
Hint Resolve Rplus_minus:
real.
Lemma Rminus_eq_contra :
forall r1 r2,
r1 <> r2 -> r1 - r2 <> 0.
#[
global]
Hint Resolve Rminus_eq_contra:
real.
Lemma Rminus_not_eq :
forall r1 r2,
r1 - r2 <> 0
-> r1 <> r2.
#[
global]
Hint Resolve Rminus_not_eq:
real.
Lemma Rminus_not_eq_right :
forall r1 r2,
r2 - r1 <> 0
-> r1 <> r2.
#[
global]
Hint Resolve Rminus_not_eq_right:
real.
Lemma Rmult_minus_distr_l :
forall r1 r2 r3,
r1 * (r2 - r3) = r1 * r2 - r1 * r3.
Lemma Rmult_minus_distr_r:
forall r1 r2 r3,
(r2 - r3) * r1 = r2 * r1 - r3 * r1.
Order and addition
Compatibility
Remark:
Rplus_lt_compat_l is an axiom
Lemma Rplus_gt_compat_l :
forall r r1 r2,
r1 > r2 -> r + r1 > r + r2.
#[
global]
Hint Resolve Rplus_gt_compat_l:
real.
Lemma Rplus_lt_compat_r :
forall r r1 r2,
r1 < r2 -> r1 + r < r2 + r.
#[
global]
Hint Resolve Rplus_lt_compat_r:
real.
Lemma Rplus_gt_compat_r :
forall r r1 r2,
r1 > r2 -> r1 + r > r2 + r.
Lemma Rplus_le_compat_l :
forall r r1 r2,
r1 <= r2 -> r + r1 <= r + r2.
Lemma Rplus_ge_compat_l :
forall r r1 r2,
r1 >= r2 -> r + r1 >= r + r2.
#[
global]
Hint Resolve Rplus_ge_compat_l:
real.
Lemma Rplus_le_compat_r :
forall r r1 r2,
r1 <= r2 -> r1 + r <= r2 + r.
#[
global]
Hint Resolve Rplus_le_compat_l Rplus_le_compat_r:
real.
Lemma Rplus_ge_compat_r :
forall r r1 r2,
r1 >= r2 -> r1 + r >= r2 + r.
Lemma Rplus_lt_compat :
forall r1 r2 r3 r4,
r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
#[
global]
Hint Immediate Rplus_lt_compat:
real.
Lemma Rplus_le_compat :
forall r1 r2 r3 r4,
r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
#[
global]
Hint Immediate Rplus_le_compat:
real.
Lemma Rplus_gt_compat :
forall r1 r2 r3 r4,
r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
Lemma Rplus_ge_compat :
forall r1 r2 r3 r4,
r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.
Lemma Rplus_lt_le_compat :
forall r1 r2 r3 r4,
r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4.
Lemma Rplus_le_lt_compat :
forall r1 r2 r3 r4,
r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
#[
global]
Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat:
real.
Lemma Rplus_gt_ge_compat :
forall r1 r2 r3 r4,
r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4.
Lemma Rplus_ge_gt_compat :
forall r1 r2 r3 r4,
r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
Lemma Rplus_lt_0_compat :
forall r1 r2, 0
< r1 -> 0
< r2 -> 0
< r1 + r2.
Lemma Rplus_le_lt_0_compat :
forall r1 r2, 0
<= r1 -> 0
< r2 -> 0
< r1 + r2.
Lemma Rplus_lt_le_0_compat :
forall r1 r2, 0
< r1 -> 0
<= r2 -> 0
< r1 + r2.
Lemma Rplus_le_le_0_compat :
forall r1 r2, 0
<= r1 -> 0
<= r2 -> 0
<= r1 + r2.
Lemma sum_inequa_Rle_lt :
forall a x b c y d:
R,
a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
Lemma Rplus_lt_reg_l :
forall r r1 r2,
r + r1 < r + r2 -> r1 < r2.
Lemma Rplus_lt_reg_r :
forall r r1 r2,
r1 + r < r2 + r -> r1 < r2.
Lemma Rplus_le_reg_l :
forall r r1 r2,
r + r1 <= r + r2 -> r1 <= r2.
Lemma Rplus_le_reg_r :
forall r r1 r2,
r1 + r <= r2 + r -> r1 <= r2.
Lemma Rplus_gt_reg_l :
forall r r1 r2,
r + r1 > r + r2 -> r1 > r2.
Lemma Rplus_ge_reg_l :
forall r r1 r2,
r + r1 >= r + r2 -> r1 >= r2.
Lemma Rplus_le_reg_pos_r :
forall r1 r2 r3, 0
<= r2 -> r1 + r2 <= r3 -> r1 <= r3.
Lemma Rplus_lt_reg_pos_r :
forall r1 r2 r3, 0
<= r2 -> r1 + r2 < r3 -> r1 < r3.
Lemma Rplus_ge_reg_neg_r :
forall r1 r2 r3, 0
>= r2 -> r1 + r2 >= r3 -> r1 >= r3.
Lemma Rplus_gt_reg_neg_r :
forall r1 r2 r3, 0
>= r2 -> r1 + r2 > r3 -> r1 > r3.
Order and opposite
Contravariant compatibility
Lemma Ropp_gt_lt_contravar :
forall r1 r2,
r1 > r2 -> - r1 < - r2.
#[
global]
Hint Resolve Ropp_gt_lt_contravar :
core.
Lemma Ropp_lt_gt_contravar :
forall r1 r2,
r1 < r2 -> - r1 > - r2.
#[
global]
Hint Resolve Ropp_lt_gt_contravar:
real.
Lemma Ropp_lt_contravar :
forall r1 r2,
r2 < r1 -> - r1 < - r2.
#[
global]
Hint Resolve Ropp_lt_contravar:
real.
Lemma Ropp_gt_contravar :
forall r1 r2,
r2 > r1 -> - r1 > - r2.
Lemma Ropp_le_ge_contravar :
forall r1 r2,
r1 <= r2 -> - r1 >= - r2.
#[
global]
Hint Resolve Ropp_le_ge_contravar:
real.
Lemma Ropp_ge_le_contravar :
forall r1 r2,
r1 >= r2 -> - r1 <= - r2.
#[
global]
Hint Resolve Ropp_ge_le_contravar:
real.
Lemma Ropp_le_contravar :
forall r1 r2,
r2 <= r1 -> - r1 <= - r2.
#[
global]
Hint Resolve Ropp_le_contravar:
real.
Lemma Ropp_ge_contravar :
forall r1 r2,
r2 >= r1 -> - r1 >= - r2.
Lemma Ropp_0_lt_gt_contravar :
forall r, 0
< r -> 0
> - r.
#[
global]
Hint Resolve Ropp_0_lt_gt_contravar:
real.
Lemma Ropp_0_gt_lt_contravar :
forall r, 0
> r -> 0
< - r.
#[
global]
Hint Resolve Ropp_0_gt_lt_contravar:
real.
Lemma Ropp_lt_gt_0_contravar :
forall r,
r > 0
-> - r < 0.
#[
global]
Hint Resolve Ropp_lt_gt_0_contravar:
real.
Lemma Ropp_gt_lt_0_contravar :
forall r,
r < 0
-> - r > 0.
#[
global]
Hint Resolve Ropp_gt_lt_0_contravar:
real.
Lemma Ropp_0_le_ge_contravar :
forall r, 0
<= r -> 0
>= - r.
#[
global]
Hint Resolve Ropp_0_le_ge_contravar:
real.
Lemma Ropp_0_ge_le_contravar :
forall r, 0
>= r -> 0
<= - r.
#[
global]
Hint Resolve Ropp_0_ge_le_contravar:
real.
Order and multiplication
Remark:
Rmult_lt_compat_l is an axiom
Covariant compatibility
Lemma Rmult_lt_compat_r :
forall r r1 r2, 0
< r -> r1 < r2 -> r1 * r < r2 * r.
#[
global]
Hint Resolve Rmult_lt_compat_r :
core.
Lemma Rmult_gt_compat_r :
forall r r1 r2,
r > 0
-> r1 > r2 -> r1 * r > r2 * r.
Lemma Rmult_gt_compat_l :
forall r r1 r2,
r > 0
-> r1 > r2 -> r * r1 > r * r2.
Lemma Rmult_le_compat_l :
forall r r1 r2, 0
<= r -> r1 <= r2 -> r * r1 <= r * r2.
#[
global]
Hint Resolve Rmult_le_compat_l:
real.
Lemma Rmult_le_compat_r :
forall r r1 r2, 0
<= r -> r1 <= r2 -> r1 * r <= r2 * r.
#[
global]
Hint Resolve Rmult_le_compat_r:
real.
Lemma Rmult_ge_compat_l :
forall r r1 r2,
r >= 0
-> r1 >= r2 -> r * r1 >= r * r2.
Lemma Rmult_ge_compat_r :
forall r r1 r2,
r >= 0
-> r1 >= r2 -> r1 * r >= r2 * r.
Lemma Rmult_le_compat :
forall r1 r2 r3 r4,
0
<= r1 -> 0
<= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
#[
global]
Hint Resolve Rmult_le_compat:
real.
Lemma Rmult_ge_compat :
forall r1 r2 r3 r4,
r2 >= 0
-> r4 >= 0
-> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
Lemma Rmult_gt_0_lt_compat :
forall r1 r2 r3 r4,
r3 > 0
-> r2 > 0
-> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
Lemma Rmult_le_0_lt_compat :
forall r1 r2 r3 r4,
0
<= r1 -> 0
<= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
Lemma Rmult_lt_0_compat :
forall r1 r2, 0
< r1 -> 0
< r2 -> 0
< r1 * r2.
Lemma Rmult_gt_0_compat :
forall r1 r2,
r1 > 0
-> r2 > 0
-> r1 * r2 > 0.
Contravariant compatibility
Lemma Rlt_minus :
forall r1 r2,
r1 < r2 -> r1 - r2 < 0.
#[
global]
Hint Resolve Rlt_minus:
real.
Lemma Rgt_minus :
forall r1 r2,
r1 > r2 -> r1 - r2 > 0.
Lemma Rlt_Rminus :
forall a b:
R,
a < b -> 0
< b - a.
Lemma Rle_minus :
forall r1 r2,
r1 <= r2 -> r1 - r2 <= 0.
Lemma Rge_minus :
forall r1 r2,
r1 >= r2 -> r1 - r2 >= 0.
Lemma Rminus_lt :
forall r1 r2,
r1 - r2 < 0
-> r1 < r2.
Lemma Rminus_gt :
forall r1 r2,
r1 - r2 > 0
-> r1 > r2.
Lemma Rminus_gt_0_lt :
forall a b, 0
< b - a -> a < b.
Lemma Rminus_le :
forall r1 r2,
r1 - r2 <= 0
-> r1 <= r2.
Lemma Rminus_ge :
forall r1 r2,
r1 - r2 >= 0
-> r1 >= r2.
Lemma tech_Rplus :
forall r (
s:
R), 0
<= r -> 0
< s -> r + s <> 0.
#[
global]
Hint Immediate tech_Rplus:
real.
Order and square function
Lemma S_INR :
forall n:
nat,
INR (
S n)
= INR n + 1.
Lemma S_O_plus_INR :
forall n:
nat,
INR (1
+ n)
= INR 1
+ INR n.
Lemma plus_INR :
forall n m:
nat,
INR (
n + m)
= INR n + INR m.
#[
global]
Hint Resolve plus_INR:
real.
Lemma minus_INR :
forall n m:
nat, (
m <= n)%
nat -> INR (
n - m)
= INR n - INR m.
#[
global]
Hint Resolve minus_INR:
real.
Lemma mult_INR :
forall n m:
nat,
INR (
n * m)
= INR n * INR m.
#[
global]
Hint Resolve mult_INR:
real.
Lemma pow_INR (
m n:
nat) :
INR (
m ^ n)
= pow (
INR m)
n.
Lemma lt_0_INR :
forall n:
nat, (0
< n)%
nat -> 0
< INR n.
#[
global]
Hint Resolve lt_0_INR:
real.
Lemma lt_INR :
forall n m:
nat, (
n < m)%
nat -> INR n < INR m.
#[
global]
Hint Resolve lt_INR:
real.
Lemma lt_1_INR :
forall n:
nat, (1
< n)%
nat -> 1
< INR n.
#[
global]
Hint Resolve lt_1_INR:
real.
Lemma pos_INR_nat_of_P :
forall p:
positive, 0
< INR (
Pos.to_nat p).
#[
global]
Hint Resolve pos_INR_nat_of_P:
real.
Lemma pos_INR :
forall n:
nat, 0
<= INR n.
#[
global]
Hint Resolve pos_INR:
real.
Lemma INR_lt :
forall n m:
nat,
INR n < INR m -> (
n < m)%
nat.
#[
global]
Hint Resolve INR_lt:
real.
Lemma le_INR :
forall n m:
nat, (
n <= m)%
nat -> INR n <= INR m.
#[
global]
Hint Resolve le_INR:
real.
Lemma INR_not_0 :
forall n:
nat,
INR n <> 0
-> n <> 0%
nat.
#[
global]
Hint Immediate INR_not_0:
real.
Lemma not_0_INR :
forall n:
nat,
n <> 0%
nat -> INR n <> 0.
#[
global]
Hint Resolve not_0_INR:
real.
Lemma not_INR :
forall n m:
nat,
n <> m -> INR n <> INR m.
#[
global]
Hint Resolve not_INR:
real.
Lemma INR_eq :
forall n m:
nat,
INR n = INR m -> n = m.
Lemma INR_le :
forall n m:
nat,
INR n <= INR m -> (
n <= m)%
nat.
#[
global]
Hint Resolve INR_le:
real.
Lemma not_1_INR :
forall n:
nat,
n <> 1%
nat -> INR n <> 1.
#[
global]
Hint Resolve not_1_INR:
real.
The three following lemmas map the default form of numerical
constants to their representation in terms of the axioms of
R. This can be a useful intermediate representation for reifying
to another axiomatics of the reals. It is however generally more
convenient to keep constants represented under an IZR z form when
working within R.
Lemma IZR_POS_xO :
forall p,
IZR (
Zpos (
xO p))
= (1
+1
) * (IZR (
Zpos p)
).
Lemma IZR_POS_xI :
forall p,
IZR (
Zpos (
xI p))
= 1
+ (1
+1
) * IZR (
Zpos p).
Lemma plus_IZR_NEG_POS :
forall p q:
positive,
IZR (
Zpos p + Zneg q)
= IZR (
Zpos p)
+ IZR (
Zneg q).
Lemma plus_IZR :
forall n m:
Z,
IZR (
n + m)
= IZR n + IZR m.
Lemma mult_IZR :
forall n m:
Z,
IZR (
n * m)
= IZR n * IZR m.
Lemma pow_IZR :
forall z n,
pow (
IZR z)
n = IZR (
Z.pow z (
Z.of_nat n)).
Lemma succ_IZR :
forall n:
Z,
IZR (
Z.succ n)
= IZR n + 1.
Lemma opp_IZR :
forall n:
Z,
IZR (
- n)
= - IZR n.
Definition Ropp_Ropp_IZR :=
opp_IZR.
Lemma minus_IZR :
forall n m:
Z,
IZR (
n - m)
= IZR n - IZR m.
Lemma Z_R_minus :
forall n m:
Z,
IZR n - IZR m = IZR (
n - m).
Lemma lt_0_IZR :
forall n:
Z, 0
< IZR n -> (0
< n)%
Z.
Lemma lt_IZR :
forall n m:
Z,
IZR n < IZR m -> (
n < m)%
Z.
Lemma eq_IZR_R0 :
forall n:
Z,
IZR n = 0
-> n = 0%
Z.
Lemma eq_IZR :
forall n m:
Z,
IZR n = IZR m -> n = m.
Lemma not_0_IZR :
forall n:
Z,
n <> 0%
Z -> IZR n <> 0.
Lemma le_0_IZR :
forall n:
Z, 0
<= IZR n -> (0
<= n)%
Z.
Lemma le_IZR :
forall n m:
Z,
IZR n <= IZR m -> (
n <= m)%
Z.
Lemma le_IZR_R1 :
forall n:
Z,
IZR n <= 1
-> (
n <= 1)%
Z.
Lemma IZR_ge :
forall n m:
Z, (
n >= m)%
Z -> IZR n >= IZR m.
Lemma IZR_le :
forall n m:
Z, (
n <= m)%
Z -> IZR n <= IZR m.
Lemma IZR_lt :
forall n m:
Z, (
n < m)%
Z -> IZR n < IZR m.
Lemma IZR_neq :
forall z1 z2:
Z,
z1 <> z2 -> IZR z1 <> IZR z2.
#[
global]
Hint Extern 0 (
IZR _ <= IZR _) =>
apply IZR_le,
Zle_bool_imp_le,
eq_refl :
real.
#[
global]
Hint Extern 0 (
IZR _ >= IZR _) =>
apply Rle_ge,
IZR_le,
Zle_bool_imp_le,
eq_refl :
real.
#[
global]
Hint Extern 0 (
IZR _ < IZR _) =>
apply IZR_lt,
eq_refl :
real.
#[
global]
Hint Extern 0 (
IZR _ > IZR _) =>
apply IZR_lt,
eq_refl :
real.
#[
global]
Hint Extern 0 (
IZR _ <> IZR _) =>
apply IZR_neq,
Zeq_bool_neq,
eq_refl :
real.
Lemma one_IZR_lt1 :
forall n:
Z, -1
< IZR n < 1
-> n = 0%
Z.
Lemma one_IZR_r_R1 :
forall r (
n m:
Z),
r < IZR n <= r + 1
-> r < IZR m <= r + 1
-> n = m.
Lemma single_z_r_R1 :
forall r (
n m:
Z),
r < IZR n -> IZR n <= r + 1
-> r < IZR m -> IZR m <= r + 1
-> n = m.
Lemma tech_single_z_r_R1 :
forall r (
n:
Z),
r < IZR n ->
IZR n <= r + 1
->
(exists s :
Z, s <> n /\ r < IZR s /\ IZR s <= r + 1
) -> False.
Lemma Rmult_le_pos :
forall r1 r2, 0
<= r1 -> 0
<= r2 -> 0
<= r1 * r2.
Lemma Rinv_le_contravar :
forall x y, 0
< x -> x <= y -> / y <= / x.
Lemma Rle_Rinv :
forall x y:
R, 0
< x -> 0
< y -> x <= y -> / y <= / x.
Lemma Ropp_div :
forall x y,
-x/y = - (x / y).
Lemma Ropp_div_den :
forall x y :
R,
y<>0
-> x / - y = - (x / y).
Lemma double :
forall r1, 2
* r1 = r1 + r1.
Lemma double_var :
forall r1,
r1 = r1 / 2
+ r1 / 2.
Lemma R_rm :
ring_morph
0%
R 1%
R Rplus Rmult Rminus Ropp eq
0%
Z 1%
Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.
Lemma Zeq_bool_IZR x y :
IZR x = IZR y -> Zeq_bool x y = true.
Add Field RField :
Rfield
(
completeness Zeq_bool_IZR,
morphism R_rm,
constants [
IZR_tac],
power_tac R_power_theory [
Rpow_tac]).
Other rules about < and <=
Lemma Rmult_ge_0_gt_0_lt_compat :
forall r1 r2 r3 r4,
r3 >= 0
-> r2 > 0
-> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
Lemma le_epsilon :
forall r1 r2,
(forall eps:
R, 0
< eps -> r1 <= r2 + eps) -> r1 <= r2.
Lemma completeness_weak :
forall E:
R -> Prop,
bound E -> (exists x :
R, E x) -> exists m :
R, is_lub E m.
Lemma Rdiv_lt_0_compat :
forall a b, 0
< a -> 0
< b -> 0
< a/b.
Lemma Rdiv_plus_distr :
forall a b c,
(a + b)/c = a/c + b/c.
Lemma Rdiv_minus_distr :
forall a b c,
(a - b)/c = a/c - b/c.
Lemma Req_EM_T :
forall r1 r2:
R,
{r1 = r2} + {r1 <> r2}.
Compatibility