Library Coquelicot.Rcomplements
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Tactic for changing the last argument of a property to an evar,
in order to apply theorems modulo equality.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This file describes basic missing facts about the standard library of reals and a few concerning ssreflect.seq. It also contains a definition of the sign function.
Ltac evar_last :=
match goal with
| |- ?f ?x ⇒
let tx := type of x in
let tx := eval simpl in tx in
let tmp := fresh "tmp" in
evar (tmp : tx) ;
refine (@eq_ind tx tmp f _ x _) ;
unfold tmp ; clear tmp
end.
Require Import Reals mathcomp.ssreflect.ssreflect.
Require Import Psatz.
Module MyNat.
Lemma neq_succ_0 (n : nat) : S n ≠ 0.
Lemma sub_succ (n m : nat) : S n - S m = n - m.
Lemma sub_succ_l (n m : nat) : n ≤ m → S m - n = S (m - n).
Lemma lt_neq (n m : nat) : n < m → n ≠ m.
Lemma minus_0_le (n m : nat) : n ≤ m → n - m = 0.
Lemma sub_succ_r (n m : nat) : n - S m = pred (n - m).
Lemma sub_add (n m : nat) : n ≤ m → m - n + n = m.
Lemma le_pred_le_succ (n m : nat) : pred n ≤ m ↔ n ≤ S m.
End MyNat.
Require Import Even Div2.
Require Import mathcomp.ssreflect.seq mathcomp.ssreflect.ssrbool.
Open Scope R_scope.
Lemma floor_ex : ∀ x : R, {n : Z | IZR n ≤ x < IZR n + 1}.
Definition floor x := proj1_sig (floor_ex x).
Lemma floor1_ex : ∀ x : R, {n : Z | IZR n < x ≤ IZR n + 1}.
Definition floor1 x := proj1_sig (floor1_ex x).
Interger part in nat
Lemma nfloor_ex : ∀ x : R, 0 ≤ x → {n : nat | INR n ≤ x < INR n + 1}.
Definition nfloor x pr := proj1_sig (nfloor_ex x pr).
Lemma nfloor1_ex : ∀ x : R, 0 < x → {n : nat | INR n < x ≤ INR n + 1}.
Definition nfloor1 x pr := proj1_sig (nfloor1_ex x pr).
More theorems about INR
Lemma INRp1_pos : ∀ n, 0 < INR n + 1.
Lemma Rlt_nat (x : R) : (∃ n : nat, x = INR (S n)) → 0 < x.
Lemma Rle_pow_lin (a : R) (n : nat) :
0 ≤ a → 1 + INR n × a ≤ (1 + a) ^ n.
Lemma C_n_n: ∀ n, C n n = 1.
Lemma C_n_0: ∀ n, C n 0 = 1.
Fixpoint pow2 (n : nat) : nat :=
match n with
| O ⇒ 1%nat
| S n ⇒ (2 × pow2 n)%nat
end.
Lemma pow2_INR (n : nat) : INR (pow2 n) = 2^n.
Lemma pow2_pos (n : nat) : (0 < pow2 n)%nat.
Lemma Rinv_le_contravar :
∀ x y, 0 < x → x ≤ y → / y ≤ / x.
Lemma Rinv_lt_cancel (x y : R) :
0 < y → / y < / x → x < y.
Lemma Rdiv_1 : ∀ x : R, x / 1 = x.
Lemma Rdiv_plus : ∀ a b c d : R, b ≠ 0 → d ≠ 0 →
a / b + c / d = (a × d + c × b) / (b × d).
Lemma Rdiv_minus : ∀ a b c d : R, b ≠ 0 → d ≠ 0 →
a / b - c / d = (a × d - c × b) / (b × d).
Order
Lemma Rplus_lt_reg_l (x y z : R) : x + y < x + z → y < z.
Lemma Rplus_lt_reg_r (x y z : R) : y + x < z + x → y < z.
Lemma Rle_div_l : ∀ a b c, c > 0 → (a / c ≤ b ↔ a ≤ b × c).
Lemma Rle_div_r : ∀ a b c, c > 0 → (a × c ≤ b ↔ a ≤ b / c).
Lemma Rlt_div_l : ∀ a b c, c > 0 → (a / c < b ↔ a < b×c).
Lemma Rlt_div_r : ∀ a b c, c > 0 → (a × c < b ↔ a < b / c).
Lemma Rdiv_lt_0_compat : ∀ r1 r2 : R, 0 < r1 → 0 < r2 → 0 < r1 / r2.
Lemma Rdiv_le_0_compat : ∀ r1 r2 : R, 0 ≤ r1 → 0 < r2 → 0 ≤ r1 / r2.
Lemma Rdiv_lt_1 : ∀ r1 r2, 0 < r2 → (r1 < r2 ↔ r1 / r2 < 1).
Lemma Rdiv_le_1 : ∀ r1 r2, 0 < r2 → (r1 ≤ r2 ↔ r1/r2 ≤ 1).
Lemma Rle_mult_Rlt : ∀ c a b : R, 0 < b → c < 1 → a ≤ b×c → a < b.
Lemma Rmult_le_0_r : ∀ a b, a ≤ 0 → 0 ≤ b → a × b ≤ 0.
Lemma Rmult_le_0_l : ∀ a b, 0 ≤ a → b ≤ 0 → a × b ≤ 0.
Lemma pow2_gt_0 (x : R) : x ≠ 0 → 0 < x ^ 2.
Lemma Rminus_eq_0 : ∀ r : R, r - r = 0.
Lemma Rdiv_minus_distr : ∀ a b c, b ≠ 0 → a / b - c = (a - b × c) / b.
Lemma Rmult_minus_distr_r: ∀ r1 r2 r3 : R, (r1 - r2) × r3 = r1 × r3 - r2 × r3.
Lemma Rminus_eq_compat_l : ∀ r r1 r2 : R, r1 = r2 ↔ r - r1 = r - r2.
Lemma Ropp_plus_minus_distr : ∀ r1 r2 : R, - (r1 + r2) = - r1 - r2.
Order
Lemma Rle_minus_l : ∀ a b c,(a - c ≤ b ↔ a ≤ b + c).
Lemma Rlt_minus_r : ∀ a b c,(a < b - c ↔ a + c < b).
Lemma Rlt_minus_l : ∀ a b c,(a - c < b ↔ a < b + c).
Lemma Rle_minus_r : ∀ a b c,(a ≤ b - c ↔ a + c ≤ b).
Lemma Rminus_le_0 : ∀ a b, a ≤ b ↔ 0 ≤ b - a.
Lemma Rminus_lt_0 : ∀ a b, a < b ↔ 0 < b - a.
Lemma sum_f_rw (a : nat → R) (n m : nat) :
(n < m)%nat → sum_f (S n) m a = sum_f_R0 a m - sum_f_R0 a n.
Lemma sum_f_rw_0 (u : nat → R) (n : nat) :
sum_f O n u = sum_f_R0 u n.
Lemma sum_f_n_Sm (u : nat → R) (n m : nat) :
(n ≤ m)%nat → sum_f n (S m) u = sum_f n m u + u (S m).
Lemma sum_f_u_Sk (u : nat → R) (n m : nat) :
(n ≤ m)%nat → sum_f (S n) (S m) u = sum_f n m (fun k ⇒ u (S k)).
Lemma sum_f_u_add (u : nat → R) (p n m : nat) :
(n ≤ m)%nat → sum_f (n + p)%nat (m + p)%nat u = sum_f n m (fun k ⇒ u (k + p)%nat).
Lemma sum_f_Sn_m (u : nat → R) (n m : nat) :
(n < m)%nat → sum_f (S n) m u = sum_f n m u - u n.
Lemma sum_f_R0_skip (u : nat → R) (n : nat) :
sum_f_R0 (fun k ⇒ u (n - k)%nat) n = sum_f_R0 u n.
Lemma sum_f_chasles (u : nat → R) (n m k : nat) :
(n < m)%nat → (m < k)%nat →
sum_f (S n) k u = sum_f (S n) m u + sum_f (S m) k u.
Lemma Rplus_max_distr_l :
∀ a b c, a + Rmax b c = Rmax (a + b) (a + c).
Lemma Rplus_max_distr_r :
∀ a b c, Rmax b c + a = Rmax (b + a) (c + a).
Lemma Rplus_min_distr_l :
∀ a b c, a + Rmin b c = Rmin (a + b) (a + c).
Lemma Rplus_min_distr_r :
∀ a b c, Rmin b c + a = Rmin (b + a) (c + a).
Lemma Rmult_max_distr_l :
∀ a b c, 0 ≤ a → a × Rmax b c = Rmax (a × b) (a × c).
Lemma Rmult_max_distr_r :
∀ a b c, 0 ≤ a → Rmax b c × a = Rmax (b × a) (c × a).
Lemma Rmult_min_distr_l :
∀ a b c, 0 ≤ a → a × Rmin b c = Rmin (a × b) (a × c).
Lemma Rmult_min_distr_r :
∀ a b c, 0 ≤ a → Rmin b c × a = Rmin (b × a) (c × a).
Lemma Rmin_assoc : ∀ x y z, Rmin x (Rmin y z) =
Rmin (Rmin x y) z.
Lemma Rmax_assoc : ∀ x y z, Rmax x (Rmax y z) =
Rmax (Rmax x y) z.
Order
Lemma Rmax_le_compat : ∀ a b c d, a ≤ b → c ≤ d → Rmax a c ≤ Rmax b d.
Lemma Rmax_opp_Rmin : ∀ a b, Rmax (-a) (-b) = - Rmin a b.
Lemma Rmin_opp_Rmax : ∀ a b, Rmin (-a) (-b) = - Rmax a b.
Lemma Rmax_mult : ∀ a b c, 0 ≤ c → Rmax a b × c = Rmax (a × c) (b × c).
Lemma Rmax_le_Rplus : ∀ a b : R, 0 ≤ a → 0 ≤ b → Rmax a b ≤ a + b.
Lemma Rplus_le_Rmax : ∀ a b : R, a + b ≤ 2×Rmax a b.
Lemma Rmin_Rmax_l : ∀ a b, Rmin a b ≤ a ≤ Rmax a b.
Lemma Rmin_Rmax_r : ∀ a b, Rmin a b ≤ b ≤ Rmax a b.
Lemma Rmin_Rmax : ∀ a b, Rmin a b ≤ Rmax a b.
Lemma Rabs_div : ∀ a b : R, b ≠ 0 → Rabs (a/b) = (Rabs a) / (Rabs b).
Lemma Rabs_eq_0 : ∀ x, Rabs x = 0 → x = 0.
Order
Lemma Rabs_le_between : ∀ x y, (Rabs x ≤ y ↔ -y ≤ x ≤ y).
Lemma Rabs_le_between' : ∀ x y z, Rabs (x - y) ≤ z ↔ y-z ≤ x ≤ y+z.
Lemma Rabs_lt_between : ∀ x y, (Rabs x < y ↔ -y < x < y).
Lemma Rabs_lt_between' : ∀ x y z, Rabs (x - y) < z ↔ y-z < x < y+z.
Lemma Rabs_le_between_min_max : ∀ x y z, Rmin x y ≤ z ≤ Rmax x y → Rabs (z - y) ≤ Rabs (x - y).
Lemma Rabs_le_between_Rmax : ∀ x m M,
m ≤ x ≤ M → Rabs x ≤ Rmax M (-m).
Lemma Rabs_lt_between_Rmax : ∀ x m M,
m < x < M → Rabs x < Rmax M (-m).
Lemma Rabs_maj2 : ∀ x, -x ≤ Rabs x.
Lemma Req_lt_aux : ∀ x y, (∀ eps : posreal, Rabs (x - y) < eps) → x = y.
Lemma Req_le_aux : ∀ x y, (∀ eps : posreal, Rabs (x - y) ≤ eps) → x = y.
Lemma is_pos_div_2 (eps : posreal) : 0 < eps / 2.
Definition pos_div_2 (eps : posreal) := mkposreal _ (is_pos_div_2 eps).
Definition sign (x : R) :=
match total_order_T 0 x with
| inleft (left _) ⇒ 1
| inleft (right _) ⇒ 0
| inright _ ⇒ -1
end.
Lemma sign_0 : sign 0 = 0.
Lemma sign_opp (x : R) : sign (-x) = - sign x.
Lemma sign_eq_1 (x : R) : 0 < x → sign x = 1.
Lemma sign_eq_m1 (x : R) : x < 0 → sign x = -1.
Lemma sign_le (x y : R) : x ≤ y → sign x ≤ sign y.
Lemma sign_ge_0 (x : R) : 0 ≤ x → 0 ≤ sign x.
Lemma sign_le_0 (x : R) : x ≤ 0 → sign x ≤ 0.
Lemma sign_neq_0 (x : R) : x ≠ 0 → sign x ≠ 0.
Lemma sign_mult (x y : R) : sign (x × y) = sign x × sign y.
Lemma sign_min_max (a b : R) :
sign (b - a) × (Rmax a b - Rmin a b) = b - a.
Lemma sum_INR : ∀ n, sum_f_R0 INR n = INR n × (INR n + 1) / 2.
Lemma interval_finite_subdiv (a b : R) (eps : posreal) : (a ≤ b) →
{l : seq R | head 0 l = a ∧ last 0 l = b ∧
∀ i, (S i < size l)%nat → nth 0 l i < nth 0 l (S i) ≤ nth 0 l i + eps}.
Lemma interval_finite_subdiv_between (a b : R) (eps : posreal) (Hab : a ≤ b) :
let l := proj1_sig (interval_finite_subdiv a b eps Hab) in
∀ i, (i < size l)%nat → a ≤ nth 0 l i ≤ b.
Notations
Lemma SSR_leq (n m : nat) : is_true (ssrnat.leq n m) ↔ (n ≤ m)%nat.
Lemma SSR_minus (n m : nat) : ssrnat.subn n m = (n - m)%nat.
Lemma SSR_minus (n m : nat) : ssrnat.subn n m = (n - m)%nat.
rcons
Lemma rcons_ind {T : Type} (P : seq T → Type) :
P [::] → (∀ (s : seq T) (t : T), P s → P (rcons s t)) → ∀ s, P s.
Lemma rcons_dec {T : Type} (P : seq T → Type) :
(P [::]) → (∀ s t, P (rcons s t)) → ∀ s, P s.
Lemma size_rcons_pos {T : Type} (s : seq T) (t : T) : (0 < size (rcons s t))%nat.
Lemma foldr_rcons {T T0 : Type} : ∀ (f : T0 → T → T) x0 s t,
foldr f x0 (rcons s t) = foldr f (f t x0) s.
Lemma foldl_rcons {T T0 : Type} : ∀ (f : T → T0 → T) x0 s t,
foldl f x0 (rcons s t) = f (foldl f x0 s) t.
Lemma head_rcons {T : Type} (x0 : T) (s : seq T) (t : T) : head x0 (rcons s t) = head t s.
Lemma behead_rcons {T : Type} (s : seq T) (t : T) :
(0 < size s)%nat → behead (rcons s t) = rcons (behead s) t.
Definition belast {T : Type} (s : seq T) :=
match s with
| [::] ⇒ [::]
| h :: s ⇒ belast h s
end.
Lemma behead_rev {T : Type} (s : seq T) : behead (rev s) = rev (belast s).
Lemma pairmap_rcons {T T0 : Type} (f : T → T → T0) (s : seq T) h0 h x0 :
pairmap f x0 (rcons (rcons s h0) h) = rcons (pairmap f x0 (rcons s h0)) (f h0 h).
Lemma map_pairmap {T T0 T1 : Type} (f : T0 → T1) (g : T → T → T0) (s : seq T) (x0 : T) :
map f (pairmap g x0 s) = pairmap (fun x y ⇒ f (g x y)) x0 s.
Lemma pairmap_map {T T0 T1 : Type} (f : T0 → T0 → T1) (g : T → T0) (s : seq T) (x0 : T) :
pairmap f (g x0) (map g s) = pairmap (fun x y ⇒ f (g x) (g y)) x0 s.
P [::] → (∀ (s : seq T) (t : T), P s → P (rcons s t)) → ∀ s, P s.
Lemma rcons_dec {T : Type} (P : seq T → Type) :
(P [::]) → (∀ s t, P (rcons s t)) → ∀ s, P s.
Lemma size_rcons_pos {T : Type} (s : seq T) (t : T) : (0 < size (rcons s t))%nat.
Lemma foldr_rcons {T T0 : Type} : ∀ (f : T0 → T → T) x0 s t,
foldr f x0 (rcons s t) = foldr f (f t x0) s.
Lemma foldl_rcons {T T0 : Type} : ∀ (f : T → T0 → T) x0 s t,
foldl f x0 (rcons s t) = f (foldl f x0 s) t.
Lemma head_rcons {T : Type} (x0 : T) (s : seq T) (t : T) : head x0 (rcons s t) = head t s.
Lemma behead_rcons {T : Type} (s : seq T) (t : T) :
(0 < size s)%nat → behead (rcons s t) = rcons (behead s) t.
Definition belast {T : Type} (s : seq T) :=
match s with
| [::] ⇒ [::]
| h :: s ⇒ belast h s
end.
Lemma behead_rev {T : Type} (s : seq T) : behead (rev s) = rev (belast s).
Lemma pairmap_rcons {T T0 : Type} (f : T → T → T0) (s : seq T) h0 h x0 :
pairmap f x0 (rcons (rcons s h0) h) = rcons (pairmap f x0 (rcons s h0)) (f h0 h).
Lemma map_pairmap {T T0 T1 : Type} (f : T0 → T1) (g : T → T → T0) (s : seq T) (x0 : T) :
map f (pairmap g x0 s) = pairmap (fun x y ⇒ f (g x y)) x0 s.
Lemma pairmap_map {T T0 T1 : Type} (f : T0 → T0 → T1) (g : T → T0) (s : seq T) (x0 : T) :
pairmap f (g x0) (map g s) = pairmap (fun x y ⇒ f (g x) (g y)) x0 s.
zip and unzip
Lemma size_unzip1 {T T0 : Type} (s : seq (T × T0)) : size (unzip1 s) = size s.
Lemma size_unzip2 {T T0 : Type} (s : seq (T × T0)) : size (unzip2 s) = size s.
Lemma zip_cons {S T : Type} hs ht (s : seq S) (t : seq T) :
zip (hs :: s) (ht :: t) = (hs,ht) :: zip s t.
Lemma zip_rcons {S T : Type} (s : seq S) (t : seq T) hs ht : size s = size t →
zip (rcons s hs) (rcons t ht) = rcons (zip s t) (hs,ht).
Lemma unzip1_rcons {S T : Type} (s : seq (S×T)) (h : S×T) :
unzip1 (rcons s h) = rcons (unzip1 s) (fst h).
Lemma unzip2_rcons {S T : Type} (s : seq (S×T)) (h : S×T) :
unzip2 (rcons s h) = rcons (unzip2 s) (snd h).
Lemma unzip1_belast {S T : Type} (s : seq (S×T)) :
unzip1 (belast s) = belast (unzip1 s).
Lemma unzip2_belast {S T : Type} (s : seq (S×T)) :
unzip2 (belast s) = belast (unzip2 s).
Lemma unzip1_behead {S T : Type} (s : seq (S×T)) :
unzip1 (behead s) = behead (unzip1 s).
Lemma unzip2_behead {S T : Type} (s : seq (S×T)) :
unzip2 (behead s) = behead (unzip2 s).
Lemma unzip1_fst {S T : Type} (s : seq (S×T)) :
unzip1 s = map (@fst S T) s.
Lemma unzip2_snd {S T : Type} (s : seq (S×T)) :
unzip2 s = map (@snd S T) s.
Lemma size_belast' {T : Type} (s : seq T) :
size (belast s) = Peano.pred (size s).
Lemma head_map {T1 T2 : Type} (f : T1 → T2) (s : seq T1) (x : T1) :
head (f x) (map f s) = f (head x s).
Lemma size_unzip2 {T T0 : Type} (s : seq (T × T0)) : size (unzip2 s) = size s.
Lemma zip_cons {S T : Type} hs ht (s : seq S) (t : seq T) :
zip (hs :: s) (ht :: t) = (hs,ht) :: zip s t.
Lemma zip_rcons {S T : Type} (s : seq S) (t : seq T) hs ht : size s = size t →
zip (rcons s hs) (rcons t ht) = rcons (zip s t) (hs,ht).
Lemma unzip1_rcons {S T : Type} (s : seq (S×T)) (h : S×T) :
unzip1 (rcons s h) = rcons (unzip1 s) (fst h).
Lemma unzip2_rcons {S T : Type} (s : seq (S×T)) (h : S×T) :
unzip2 (rcons s h) = rcons (unzip2 s) (snd h).
Lemma unzip1_belast {S T : Type} (s : seq (S×T)) :
unzip1 (belast s) = belast (unzip1 s).
Lemma unzip2_belast {S T : Type} (s : seq (S×T)) :
unzip2 (belast s) = belast (unzip2 s).
Lemma unzip1_behead {S T : Type} (s : seq (S×T)) :
unzip1 (behead s) = behead (unzip1 s).
Lemma unzip2_behead {S T : Type} (s : seq (S×T)) :
unzip2 (behead s) = behead (unzip2 s).
Lemma unzip1_fst {S T : Type} (s : seq (S×T)) :
unzip1 s = map (@fst S T) s.
Lemma unzip2_snd {S T : Type} (s : seq (S×T)) :
unzip2 s = map (@snd S T) s.
Lemma size_belast' {T : Type} (s : seq T) :
size (belast s) = Peano.pred (size s).
Lemma head_map {T1 T2 : Type} (f : T1 → T2) (s : seq T1) (x : T1) :
head (f x) (map f s) = f (head x s).
Lemma StepFun_bound {a b : R} (f : StepFun a b) :
∃ s : R, ∀ x, Rmin a b ≤ x ≤ Rmax a b → f x ≤ s.
Lemma Riemann_integrable_bound (f : R → R) (a b : R) :
Riemann_integrable f a b → ∃ s : R, ∀ x, Rmin a b ≤ x ≤ Rmax a b → f x ≤ s.
Extensionality
Lemma Riemann_integrable_ext : ∀ (f g : R → R) (a b : R),
(∀ x, Rmin a b ≤ x ≤ Rmax a b → f x = g x)
→ Riemann_integrable f a b → Riemann_integrable g a b.
Lemma RiemannInt_ext : ∀ (f g : R → R) (a b : R)
(pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b)
(Heq : ∀ x, Rmin a b ≤ x ≤ Rmax a b → f x = g x),
RiemannInt pr_f = RiemannInt pr_g.
Constant function
Lemma Riemann_integrable_const : ∀ (c a b : R),
Riemann_integrable (fun x ⇒ c) a b.
Lemma RiemannInt_const : ∀ (c a b : R) (pr : Riemann_integrable (fun x ⇒ c) a b),
RiemannInt pr = c × (b-a).
Addition
Lemma Riemann_integrable_plus : ∀ (f g : R → R) (a b : R),
Riemann_integrable f a b → Riemann_integrable g a b →
Riemann_integrable (fun x ⇒ f x + g x) a b.
Lemma RiemannInt_plus : ∀ (f g : R → R) (a b : R)
(pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b)
(pr : Riemann_integrable (fun x ⇒ f x + g x) a b),
RiemannInt pr = RiemannInt pr_f + RiemannInt pr_g.
Subtraction
Lemma Riemann_integrable_minus : ∀ (f g : R → R) (a b : R),
Riemann_integrable f a b → Riemann_integrable g a b →
Riemann_integrable (fun x ⇒ f x - g x) a b.
Lemma RiemannInt_minus : ∀ (f g : R → R) (a b : R)
(pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b)
(pr : Riemann_integrable (fun x ⇒ f x - g x) a b),
RiemannInt pr = RiemannInt pr_f - RiemannInt pr_g.
Opposite
Lemma Riemann_integrable_opp : ∀ (f : R → R) (a b : R),
Riemann_integrable f a b →
Riemann_integrable (fun x ⇒ - f x) a b.
Lemma RiemannInt_opp : ∀ (f : R → R) (a b : R)
(pr_f : Riemann_integrable f a b)
(pr : Riemann_integrable (fun x ⇒ - f x) a b),
RiemannInt pr = - RiemannInt pr_f.
Multiplication by a scalar
Lemma Riemann_integrable_scal : ∀ (f : R → R) (a b c : R),
Riemann_integrable f a b →
Riemann_integrable (fun x ⇒ c × f x) a b.
Lemma RiemannInt_scal : ∀ (f : R → R) (a b c : R)
(pr_f : Riemann_integrable f a b)
(pr : Riemann_integrable (fun x ⇒ c × f x) a b),
RiemannInt pr = c × RiemannInt pr_f.