Théorèmes sur les réels (type R)

Divers
Req_dec : ∀ r1 r2 : R, r1 = r2 ∨ r1 ≠ r2
R1_neq_R0 : 1 ≠ 0

Addition (Rplus), opposé (Ropp), soustraction (Rminus)
Rplus_eq_compat_r : ∀ r r1 r2 : R, r1 = r2 → r1 + r = r2 + r
Rplus_eq_compat_l : ∀ r r1 r2 : R, r1 = r2 → r + r1 = r + r2
Rplus_comm : ∀ r1 r2 : R, r1 + r2 = r2 + r1
Rplus_assoc : ∀ r1 r2 r3 : R, r1 + r2 + r3 = r1 + (r2 + r3)
Rplus_0_l : ∀ r : R, 0 + r = r
Rplus_0_r : ∀ r : R, r + 0 = r
Rplus_opp_l : ∀ r : R, - r + r = 0
Rplus_opp_r : ∀ r : R, r + - r = 0
Rplus_eq_reg_r : ∀ r r1 r2 : R, r + r1 = r + r2 → r1 = r2
Rplus_eq_reg_l : ∀ r r1 r2 : R, r1 + r = r2 + r → r1 = r2
Ropp_involutive : ∀ r : R, - - r = r
Ropp_0 : - 0 = 0
Rminus = λ r1 r2 : R, r1 + - r2 : R → R → R
Rminus_0_l : ∀ r : R, 0 - r = - r
Rminus_0_r : ∀ r : R, r - 0 = r
Rminus_diag_uniq : ∀ r1 r2 : R, r1 - r2 = 0 → r1 = r2

Multiplication (Rmult), inverse (Rinv), division (Rdiv)
Rmult_eq_compat_r : ∀ r r1 r2 : R, r1 = r2 → r1 * r = r2 * r
Rmult_eq_compat_l : ∀ r r1 r2 : R, r1 = r2 → r * r1 = r * r2
Rmult_assoc : ∀ r1 r2 r3 : R, r1 * r2 * r3 = r1 * (r2 * r3)
Rmult_comm : ∀ r1 r2 : R, r1 * r2 = r2 * r1
Rmult_1_r : ∀ r : R, r * 1 = r
Rmult_1_l : ∀ r : R, 1 * r = r
Rmult_plus_distr_l : ∀ r1 r2 r3 : R, r1 * (r2 + r3) = r1 * r2 + r1 * r3
Rmult_plus_distr_r : ∀ r1 r2 r3 : R, (r1 + r2) * r3 = r1 * r3 + r2 * r3
Rmult_0_r : ∀ r : R, r * 0 = 0
Rmult_0_l : ∀ r : R, 0 * r = 0
Rmult_opp_opp : ∀ r1 r2 : R, - r1 * - r2 = r1 * r2
Rinv_inv : ∀ r : R, / / r = r
Rinv_l : ∀ r : R, r ≠ 0 → / r * r = 1
Rinv_r : ∀ r : R, r ≠ 0 → r * / r = 1
Rmult_eq_reg_l : ∀ r r1 r2 : R, r * r1 = r * r2 → r ≠ 0 → r1 = r2
Rmult_eq_reg_r : ∀ r r1 r2 : R, r1 * r = r2 * r → r ≠ 0 → r1 = r2
Rmult_integral : ∀ r1 r2 : R, r1 * r2 = 0 → r1 = 0 ∨ r2 = 0
Rinv_div : ∀ x y : R, / (x / y) = y / x
Rinv_neq_0_compat : ∀ r : R, r ≠ 0 → / r ≠ 0
double : ∀ r1 : R, 2 * r1 = r1 + r1

Ordre < (Rlt)
Rlt_asym : ∀ r1 r2 : R, r1 < r2 → ¬ r2 < r1
Rlt_trans : ∀ r1 r2 r3 : R, r1 < r2 → r2 < r3 → r1 < r3
Rlt_irrefl : ∀ r : R, ¬ r < r
Rplus_lt_compat_l : ∀ r r1 r2 : R, r1 < r2 → r + r1 < r + r2
Rplus_lt_compat_r : ∀ r r1 r2 : R, r1 < r2 → r1 + r < r2 + r
Rplus_lt_compat : ∀ r1 r2 r3 r4 : R, r1 < r2 → r3 < r4 → r1 + r3 < r2 + r4
Rmult_lt_compat_l : ∀ r r1 r2 : R, 0 < r → r1 < r2 → r * r1 < r * r2
Rmult_lt_compat_r : ∀ r r1 r2 : R, 0 < r → r1 < r2 → r1 * r < r2 * r
Ropp_lt_contravar : ∀ r1 r2 : R, r2 < r1 → - r1 < - r2
Rdiv_lt_0_compat : ∀ a b : R, 0 < a → 0 < b → 0 < a / b
total_order_T : ∀ r1 r2 : R, {r1 < r2} + {r1 = r2} + {r2 < r1}
Ropp_lt_contravar : ∀ r1 r2 : R, r2 < r1 → - r1 < - r2
Rinv_0_lt_compat : ∀ r : R, 0 < r → 0 < / r
Rlt_plus_1 : ∀ r : R, r < r + 1
Rlt_0_1 : 0 < 1
Rlt_0_2 : 0 < 2
Rinv_lt_contravar : ∀ r1 r2 : R, 0 < r1 * r2 → r1 < r2 → / r2 < / r1

Ordre <= (Rle)
Rle = λ r1 r2 : R, r1 < r2 ∨ r1 = r2 : R → R → Prop
Rle_trans : ∀ r1 r2 r3 : R, r1 <= r2 → r2 <= r3 → r1 <= r3
Rle_refl : ∀ r : R, r <= r
Rle_antisym : ∀ r1 r2 : R, r1 <= r2 → r2 <= r1 → r1 = r2
Rplus_le_compat_l : ∀ r r1 r2 : R, r1 <= r2 → r + r1 <= r + r2
Rplus_le_compat_r : ∀ r r1 r2 : R, r1 <= r2 → r1 + r <= r2 + r
Rplus_le_compat : ∀ r1 r2 r3 r4 : R, r1 <= r2 → r3 <= r4 → r1 + r3 <= r2 + r4
Rmult_le_compat_l : ∀ r r1 r2 : R, 0 <= r → r1 <= r2 → r * r1 <= r * r2
Rmult_le_compat_r : ∀ r r1 r2 : R, 0 <= r → r1 <= r2 → r1 * r <= r2 * r
Rlt_le : ∀ r1 r2 : R, r1 < r2 → r1 <= r2
Rlt_or_le : ∀ r1 r2 : R, r1 < r2 ∨ r2 <= r1
Rle_not_lt : ∀ r1 r2 : R, r2 <= r1 → ¬ r1 < r2
Req_le_sym : ∀ r1 r2 : R, r2 = r1 → r1 <= r2
Rle_lt_trans : ∀ r1 r2 r3 : R, r1 <= r2 → r2 < r3 → r1 < r3
Rlt_le_trans : ∀ r1 r2 r3 : R, r1 < r2 → r2 <= r3 → r1 < r3
Rplus_le_lt_0_compat : ∀ r1 r2 : R, 0 <= r1 → 0 < r2 → 0 < r1 + r2
Rmult_le_pos : ∀ r1 r2 : R, 0 <= r1 → 0 <= r2 → 0 <= r1 * r2

Ordre > (Rgt)
Rgt = λ r1 r2 : R, r2 < r1 : R → R → Prop
Rmult_gt_0_compat : ∀ r1 r2 : R, r1 > 0 → r2 > 0 → r1 * r2 > 0
Rgt_trans : ∀ r1 r2 r3 : R, r1 > r2 → r2 > r3 → r1 > r3
Ropp_gt_lt_0_contravar : ∀ r : R, r < 0 → - r > 0
Rmult_gt_0_lt_compat : ∀ r1 r2 r3 r4 : R,
         r3 > 0 → r2 > 0 → r1 < r2 → r3 < r4 → r1 * r3 < r2 * r4

Ordre >= (Rge)
Rge = λ r1 r2 : R, r1 > r2 ∨ r1 = r2 : R → R → Prop
Rle_ge : ∀ r1 r2 : R, r1 <= r2 → r2 >= r1
Rge_le : ∀ r1 r2 : R, r1 >= r2 → r2 <= r1

Fonction carré (Rsqr)
Rsqr = λ r : R, r * r : R → R
Rle_0_sqr : ∀ r : R, 0 <= r²
Rsqr_neg : ∀ x : R, x² = (- x)²
Rsqr_incrst_1 : ∀ x y : R, x < y → 0 <= x → 0 <= y → x² < y²
Rsqr_inj : ∀ x y : R, 0 <= x → 0 <= y → x² = y² → x = y
Rsqr_mult : ∀ x y : R, (x * y)² = x² * y²
Rsqr_incr_0_var : ∀ x y : R, x² <= y² → 0 <= y → x <= y

Valeur absolue (Rabs)
Rcase_abs : ∀ r : R, {r < 0} + {r >= 0}
Rabs = λ r : R, if Rcase_abs r then - r else r : R → R
Rabs_pos : ∀ x : R, 0 <= Rabs x
Rabs_pos_lt : ∀ x : R, x ≠ 0 → 0 < Rabs x
Rle_abs : ∀ x : R, x <= Rabs x
Rabs_left : ∀ r : R, r < 0 → Rabs r = - r
Rabs_right : ∀ r : R, r >= 0 → Rabs r = r
Rabs_R0 : Rabs 0 = 0
Rabs_Ropp : ∀ x : R, Rabs (- x) = Rabs x
Rabs_mult : ∀ x y : R, Rabs (x * y) = Rabs x * Rabs y

Distance (R_dist)
R_dist = λ x y : R, Rabs (x - y) : R → R → R
R_dist_pos : ∀ x y : R, R_dist x y >= 0
R_dist_sym : ∀ x y : R, R_dist x y = R_dist y x
R_dist_refl : ∀ x y : R, R_dist x y = 0 ↔ x = y
R_dist_eq : ∀ x : R, R_dist x x = 0
R_dist_tri : ∀ x y z : R, R_dist x y <= R_dist x z + R_dist z y
R_dist_mult_l : ∀ a b c : R, R_dist (a * b) (a * c) = Rabs a * R_dist b c
R_dist_plus : ∀ a b c d : R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d

Injection de nat dans R (INR)
le_INR : ∀ n m : nat, n ≤ m → INR n <= INR m
pos_INR : ∀ n : nat, 0 <= INR n