Library Coq.Reals.RIneq
Basic lemmas for the classical real numbers
Relation between orders and equality
Reflexivity of the large order
Irreflexivity of the strict order
Reasoning by case on equality and order
Lemma Req_dec :
forall r1 r2,
r1 =
r2 \/
r1 <>
r2.
Hint Resolve Req_dec:
real.
Lemma Rtotal_order :
forall r1 r2,
r1 <
r2 \/
r1 =
r2 \/
r1 >
r2.
Lemma Rdichotomy :
forall r1 r2,
r1 <>
r2 ->
r1 <
r2 \/
r1 >
r2.
Relating strict and large orders
Lemma Rlt_le :
forall r1 r2,
r1 <
r2 ->
r1 <=
r2.
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.
Hint Immediate Rle_ge:
real.
Hint Resolve Rle_ge:
rorders.
Lemma Rge_le :
forall r1 r2,
r1 >=
r2 ->
r2 <=
r1.
Hint Resolve Rge_le:
real.
Hint Immediate Rge_le:
rorders.
Lemma Rlt_gt :
forall r1 r2,
r1 <
r2 ->
r2 >
r1.
Hint Resolve Rlt_gt:
rorders.
Lemma Rgt_lt :
forall r1 r2,
r1 >
r2 ->
r2 <
r1.
Hint Immediate Rgt_lt:
rorders.
Lemma Rnot_le_lt :
forall r1 r2, ~
r1 <=
r2 ->
r2 <
r1.
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.
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.
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.
Hint Immediate Req_le:
real.
Lemma Req_ge :
forall r1 r2,
r1 =
r2 ->
r1 >=
r2.
Hint Immediate Req_ge:
real.
Lemma Req_le_sym :
forall r1 r2,
r2 =
r1 ->
r1 <=
r2.
Hint Immediate Req_le_sym:
real.
Lemma Req_ge_sym :
forall r1 r2,
r2 =
r1 ->
r1 >=
r2.
Hint Immediate Req_ge_sym:
real.
Remark: Rlt_asym is an axiom
Lemma Rgt_asym :
forall r1 r2:R,
r1 >
r2 -> ~
r2 >
r1.
Lemma Rle_antisym :
forall r1 r2,
r1 <=
r2 ->
r2 <=
r1 ->
r1 =
r2.
Hint Resolve Rle_antisym:
real.
Lemma Rge_antisym :
forall r1 r2,
r1 >=
r2 ->
r2 >=
r1 ->
r1 =
r2.
Lemma Rle_le_eq :
forall r1 r2,
r1 <=
r2 /\
r2 <=
r1 <->
r1 =
r2.
Lemma Rge_ge_eq :
forall r1 r2,
r1 >=
r2 /\
r2 >=
r1 <->
r1 =
r2.
Compatibility with equality
Lemma Rlt_eq_compat :
forall r1 r2 r3 r4,
r1 =
r2 ->
r2 <
r4 ->
r4 =
r3 ->
r1 <
r3.
Lemma Rgt_eq_compat :
forall r1 r2 r3 r4,
r1 =
r2 ->
r2 >
r4 ->
r4 =
r3 ->
r1 >
r3.
Remark: Rlt_trans is an axiom
Lemma Rle_trans :
forall r1 r2 r3,
r1 <=
r2 ->
r2 <=
r3 ->
r1 <=
r3.
Lemma Rge_trans :
forall r1 r2 r3,
r1 >=
r2 ->
r2 >=
r3 ->
r1 >=
r3.
Lemma Rgt_trans :
forall r1 r2 r3,
r1 >
r2 ->
r2 >
r3 ->
r1 >
r3.
Lemma Rle_lt_trans :
forall r1 r2 r3,
r1 <=
r2 ->
r2 <
r3 ->
r1 <
r3.
Lemma Rlt_le_trans :
forall r1 r2 r3,
r1 <
r2 ->
r2 <=
r3 ->
r1 <
r3.
Lemma Rge_gt_trans :
forall r1 r2 r3,
r1 >=
r2 ->
r2 >
r3 ->
r1 >
r3.
Lemma Rgt_ge_trans :
forall r1 r2 r3,
r1 >
r2 ->
r2 >=
r3 ->
r1 >
r3.
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}.
Remark: Rplus_0_l is an axiom
Remark: Rplus_opp_r is an axiom
Lemma Rinv_r :
forall r,
r <> 0 ->
r * /
r = 1.
Hint Resolve Rinv_r:
real.
Lemma Rinv_l_sym :
forall r,
r <> 0 -> 1 = /
r *
r.
Hint Resolve Rinv_l_sym:
real.
Lemma Rinv_r_sym :
forall r,
r <> 0 -> 1 =
r * /
r.
Hint Resolve Rinv_r_sym:
real.
Lemma Rmult_0_r :
forall r,
r * 0 = 0.
Hint Resolve Rmult_0_r:
real v62.
Lemma Rmult_0_l :
forall r, 0 *
r = 0.
Hint Resolve Rmult_0_l:
real v62.
Lemma Rmult_ne :
forall r,
r * 1 =
r /\ 1 *
r =
r.
Hint Resolve Rmult_ne:
real v62.
Lemma Rmult_1_r :
forall r,
r * 1 =
r.
Hint Resolve Rmult_1_r:
real.
Lemma Rmult_eq_compat_l :
forall r r1 r2,
r1 =
r2 ->
r *
r1 =
r *
r2.
Hint Resolve Rmult_eq_compat_l:
v62.
Lemma Rmult_eq_reg_l :
forall r r1 r2,
r *
r1 =
r *
r2 ->
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.
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.
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.
Definition Rsqr r :
R :=
r *
r.
Notation "r ²" := (
Rsqr r) (
at level 1,
format "r ²") :
R_scope.
Lemma Rsqr_0 :
Rsqr 0 = 0.
Lemma Rsqr_0_uniq :
forall r,
Rsqr r = 0 ->
r = 0.
Opposite and multiplication
Lemma Rminus_0_r :
forall r,
r - 0 =
r.
Hint Resolve Rminus_0_r:
real.
Lemma Rminus_0_l :
forall r, 0 -
r = -
r.
Hint Resolve Rminus_0_l:
real.
Lemma Ropp_minus_distr :
forall r1 r2, - (
r1 -
r2) =
r2 -
r1.
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.
Hint Resolve Rminus_diag_eq:
real.
Lemma Rminus_diag_uniq :
forall r1 r2,
r1 -
r2 = 0 ->
r1 =
r2.
Hint Immediate Rminus_diag_uniq:
real.
Lemma Rminus_diag_uniq_sym :
forall r1 r2,
r2 -
r1 = 0 ->
r1 =
r2.
Hint Immediate Rminus_diag_uniq_sym:
real.
Lemma Rplus_minus :
forall r1 r2,
r1 + (
r2 -
r1) =
r2.
Hint Resolve Rplus_minus:
real.
Lemma Rminus_eq_contra :
forall r1 r2,
r1 <>
r2 ->
r1 -
r2 <> 0.
Hint Resolve Rminus_eq_contra:
real.
Lemma Rminus_not_eq :
forall r1 r2,
r1 -
r2 <> 0 ->
r1 <>
r2.
Hint Resolve Rminus_not_eq:
real.
Lemma Rminus_not_eq_right :
forall r1 r2,
r2 -
r1 <> 0 ->
r1 <>
r2.
Hint Resolve Rminus_not_eq_right:
real.
Lemma Rmult_minus_distr_l :
forall r1 r2 r3,
r1 * (
r2 -
r3) =
r1 *
r2 -
r1 *
r3.
Remark: Rplus_lt_compat_l is an axiom
Lemma Rplus_gt_compat_l :
forall r r1 r2,
r1 >
r2 ->
r +
r1 >
r +
r2.
Hint Resolve Rplus_gt_compat_l:
real.
Lemma Rplus_lt_compat_r :
forall r r1 r2,
r1 <
r2 ->
r1 +
r <
r2 +
r.
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.
Hint Resolve Rplus_ge_compat_l:
real.
Lemma Rplus_le_compat_r :
forall r r1 r2,
r1 <=
r2 ->
r1 +
r <=
r2 +
r.
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.
Hint Immediate Rplus_lt_compat:
real.
Lemma Rplus_le_compat :
forall r1 r2 r3 r4,
r1 <=
r2 ->
r3 <=
r4 ->
r1 +
r3 <=
r2 +
r4.
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.
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.
Contravariant compatibility
Lemma Ropp_gt_lt_contravar :
forall r1 r2,
r1 >
r2 -> -
r1 < -
r2.
Hint Resolve Ropp_gt_lt_contravar.
Lemma Ropp_lt_gt_contravar :
forall r1 r2,
r1 <
r2 -> -
r1 > -
r2.
Hint Resolve Ropp_lt_gt_contravar:
real.
Lemma Ropp_lt_contravar :
forall r1 r2,
r2 <
r1 -> -
r1 < -
r2.
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.
Hint Resolve Ropp_le_ge_contravar:
real.
Lemma Ropp_ge_le_contravar :
forall r1 r2,
r1 >=
r2 -> -
r1 <= -
r2.
Hint Resolve Ropp_ge_le_contravar:
real.
Lemma Ropp_le_contravar :
forall r1 r2,
r2 <=
r1 -> -
r1 <= -
r2.
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.
Hint Resolve Ropp_0_lt_gt_contravar:
real.
Lemma Ropp_0_gt_lt_contravar :
forall r, 0 >
r -> 0 < -
r.
Hint Resolve Ropp_0_gt_lt_contravar:
real.
Lemma Ropp_lt_gt_0_contravar :
forall r,
r > 0 -> -
r < 0.
Hint Resolve Ropp_lt_gt_0_contravar:
real.
Lemma Ropp_gt_lt_0_contravar :
forall r,
r < 0 -> -
r > 0.
Hint Resolve Ropp_gt_lt_0_contravar:
real.
Lemma Ropp_0_le_ge_contravar :
forall r, 0 <=
r -> 0 >= -
r.
Hint Resolve Ropp_0_le_ge_contravar:
real.
Lemma Ropp_0_ge_le_contravar :
forall r, 0 >=
r -> 0 <= -
r.
Hint Resolve Ropp_0_ge_le_contravar:
real.
Remark: Rmult_lt_compat_l is an axiom
Lemma Rmult_lt_compat_r :
forall r r1 r2, 0 <
r ->
r1 <
r2 ->
r1 *
r <
r2 *
r.
Hint Resolve Rmult_lt_compat_r.
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.
Hint Resolve Rmult_le_compat_l:
real.
Lemma Rmult_le_compat_r :
forall r r1 r2, 0 <=
r ->
r1 <=
r2 ->
r1 *
r <=
r2 *
r.
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.
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 Rmult_lt_reg_l :
forall r r1 r2, 0 <
r ->
r *
r1 <
r *
r2 ->
r1 <
r2.
Lemma Rmult_gt_reg_l :
forall r r1 r2, 0 <
r ->
r *
r1 <
r *
r2 ->
r1 <
r2.
Lemma Rmult_le_reg_l :
forall r r1 r2, 0 <
r ->
r *
r1 <=
r *
r2 ->
r1 <=
r2.
Lemma Rlt_minus :
forall r1 r2,
r1 <
r2 ->
r1 -
r2 < 0.
Hint Resolve Rlt_minus:
real.
Lemma Rgt_minus :
forall r1 r2,
r1 >
r2 ->
r1 -
r2 > 0.
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_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.
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.
Hint Resolve plus_INR:
real.
Lemma minus_INR :
forall n m:nat, (
m <=
n)%nat ->
INR (
n -
m) =
INR n -
INR m.
Hint Resolve minus_INR:
real.
Lemma mult_INR :
forall n m:nat,
INR (
n *
m) =
INR n *
INR m.
Hint Resolve mult_INR:
real.
Lemma lt_0_INR :
forall n:nat, (0 <
n)%nat -> 0 <
INR n.
Hint Resolve lt_0_INR:
real.
Lemma lt_INR :
forall n m:nat, (
n <
m)%nat ->
INR n <
INR m.
Hint Resolve lt_INR:
real.
Lemma lt_1_INR :
forall n:nat, (1 <
n)%nat -> 1 <
INR n.
Hint Resolve lt_1_INR:
real.
Lemma pos_INR_nat_of_P :
forall p:positive, 0 <
INR (
nat_of_P p).
Hint Resolve pos_INR_nat_of_P:
real.
Lemma pos_INR :
forall n:nat, 0 <=
INR n.
Hint Resolve pos_INR:
real.
Lemma INR_lt :
forall n m:nat,
INR n <
INR m -> (
n <
m)%nat.
Hint Resolve INR_lt:
real.
Lemma le_INR :
forall n m:nat, (
n <=
m)%nat ->
INR n <=
INR m.
Hint Resolve le_INR:
real.
Lemma INR_not_0 :
forall n:nat,
INR n <> 0 ->
n <> 0%nat.
Hint Immediate INR_not_0:
real.
Lemma not_0_INR :
forall n:nat,
n <> 0%nat ->
INR n <> 0.
Hint Resolve not_0_INR:
real.
Lemma not_INR :
forall n m:nat,
n <>
m ->
INR n <>
INR m.
Hint Resolve not_INR:
real.
Lemma INR_eq :
forall n m:nat,
INR n =
INR m ->
n =
m.
Hint Resolve INR_eq:
real.
Lemma INR_le :
forall n m:nat,
INR n <=
INR m -> (
n <=
m)%nat.
Hint Resolve INR_le:
real.
Lemma not_1_INR :
forall n:nat,
n <> 1%nat ->
INR n <> 1.
Hint Resolve not_1_INR:
real.
Lemma IZN :
forall n:Z, (0 <=
n)%Z ->
exists m :
nat,
n =
Z_of_nat m.
Lemma INR_IZR_INZ :
forall n:nat,
INR n =
IZR (
Z_of_nat n).
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 (
Zpower z (
Z_of_nat n)).
Lemma succ_IZR :
forall n:Z,
IZR (
Zsucc n) =
IZR n + 1.
Lemma Ropp_Ropp_IZR :
forall n:Z,
IZR (-
n) = -
IZR n.
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 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 double :
forall r1, 2 *
r1 =
r1 +
r1.
Lemma double_var :
forall r1,
r1 =
r1 / 2 +
r1 / 2.
Other rules about < and <=
Compatibility