(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
Require Import BinPos.
From mathcomp Require choice.
(* Missing coercion (done before Import to avoid redeclaration error,
   thanks to KS for the trick) *)
(* MathComp 1.15 addition *)
Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of.

From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From mathcomp Require Import finset interval.

(***************************)
(* MathComp 1.15 additions *)
(***************************)

(******************************************************************************)
(* This files contains lemmas and definitions missing from MathComp.          *)
(*                                                                            *)
(*               f \max g := fun x => Num.max (f x) (g x)                     *)
(*                oflit f := Some \o f                                        *)
(*          pred_oapp T D := [pred x | oapp (mem D) false x]                  *)
(*                 f \* g := fun x => f x * g x                               *)
(*                   \- f := fun x => - f x                                   *)
(*     lteBSide, bnd_simp == multirule to simplify inequalities between       *)
(*                           interval bounds                                  *)
(*               miditv i == middle point of interval i                       *)
(*                                                                            *)
(*               proj i f == f i, where f : forall i, T i                     *)
(*             dfwith f x == fun j => x if j = i, and f j otherwise           *)
(*                           given x : T i                                    *)
(*                 swap x := (x.2, x.1)                                       *)
(*                                                                            *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "f \- g" (at level 50, left associativity).
Reserved Notation "\- f"  (at level 35, f at level 35).
Reserved Notation "f \max g" (at level 50, left associativity).

Number Notation positive Pos.of_num_int Pos.to_num_uint : AC_scope.

Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I)
   (P Q : I -> T -> Prop) : T ->
    (forall x : I, D x -> {y : T | P x y & Q x y}) ->
  {f : forall x : I, T | forall x : I, D x -> P x (f x) & forall x : I, D x -> Q x (f x)}.
I, T: Type
D: pred I
P, Q: I -> T -> Prop
T ->
(forall x : I, D x -> {y : T | P x y & Q x y}) ->
{f : I -> T | forall x : I, D x -> P x (f x) &
forall x : I, D x -> Q x (f x)}
Proof.
2
by move=> /all_sig_cond/[apply]-[f Pf]; exists f => i Di; have [] := Pf i Di.
Qed.

Definition olift aT rT (f : aT -> rT) := Some \o f.

Lemma oapp_comp aT rT sT (f : aT -> rT) (g : rT -> sT) x :
  oapp (g \o f) x =1 (@oapp _ _)^~ x g \o omap f.
aT, rT, sT: Type
f: aT -> rT
g: rT -> sT
x: sT
oapp (g \o f) x =1 ((oapp (rT:=sT))^~ x) g \o omap f
Proof.
b by case. Qed.

Lemma olift_comp aT rT sT (f : aT -> rT) (g : rT -> sT) :
  olift (g \o f) = olift g \o f.
e
f
10
olift (g \o f) = olift g \o f
Proof.
15 by []. Qed.

Lemma compA {A B C D : Type} (f : B -> A) (g : C -> B) (h : D -> C) :
  f \o (g \o h) = (f \o g) \o h.
A, B, C, D: Type
f: B -> A
g: C -> B
h: D -> C
f \o (g \o h) = (f \o g) \o h
Proof.
1b by []. Qed.

Lemma can_in_pcan [rT aT : Type] (A : {pred aT}) [f : aT -> rT] [g : rT -> aT] :
  {in A, cancel f g} -> {in A, pcancel f (fun y : rT => Some (g y))}.
rT, aT: Type
A: {pred aT}
f
g: rT -> aT
{in A, cancel f g} ->
{in A, pcancel f (fun y : rT => Some (g y))}
Proof.
25 by move=> fK x Ax; rewrite fK. Qed.

Lemma pcan_in_inj [rT aT : Type] [A : {pred aT}] [f : aT -> rT] [g : rT -> option aT] :
  {in A, pcancel f g} -> {in A &, injective f}.
28
29
f
g: rT -> option aT
{in A, pcancel f g} -> {in A &, injective f}
Proof.
2e by move=> fK x y Ax Ay /(congr1 g); rewrite !fK// => -[]. Qed.

Definition pred_oapp T (D : {pred T}) : pred (option T) :=
  [pred x | oapp (mem D) false x].

Lemma ocan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
    [f : B -> option A] [h : C -> option B]
    [f' : A -> B] [h' : B -> C] :
  {homo h : x / x \in D' >-> x \in pred_oapp D} ->
  {in D, ocancel f f'} -> {in D', ocancel h h'} ->
  {in D', ocancel (obind f \o h) (h' \o f')}.
A, B, C: Type
D: {pred B}
D': {pred C}
f: B -> option A
h: C -> option B
f': A -> B
h': B -> C
{homo h : x / x \in D' >-> x \in pred_oapp D} ->
{in D, ocancel f f'} ->
{in D', ocancel h h'} ->
{in D', ocancel (obind f \o h) (h' \o f')}
Proof.
35
move=> hD fK hK c cD /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=.
38
39
3a
3b
3c
3d
3e
hD: {homo h : x / x \in D' >-> x \in pred_oapp D}
fK: {in D, ocancel f f'}
hK: {in D', ocancel h h'}
c: C
cD: c \in D'
b: B
hcE: h c = Some b
oapp (h' \o f') c (f b) = h' b
have bD : b \in D by have := hD _ cD; rewrite hcE inE.
38
39
3a
3b
3c
3d
3e
45
46
47
48
49
4a
4b
bD: b \in D
4c
by rewrite -[b in RHS]fK; case: (f b) => //=; have /hK := cD; rewrite hcE.
Qed.

Lemma eqbRL (b1 b2 : bool) : b1 = b2 -> b2 -> b1.
b1, b2: bool
b1 = b2 -> b2 -> b1
Proof.
53 by move->. Qed.

Definition mul_fun T (R : ringType) (f g : T -> R) x := (f x * g x)%R.
Notation "f \* g" := (mul_fun f g) : ring_scope.
Notation "_ \* _" was already used in scope
ring_scope. [notation-overridden,parsing]
Arguments mul_fun {T R} _ _ _ /.

Definition opp_fun T (R : zmodType) (f : T -> R) x := (- f x)%R.
Notation "\- f" := (opp_fun f) : ring_scope.
Notation "\- _" was already used in scope ring_scope.
[notation-overridden,parsing]
Arguments opp_fun {T R} _ _ /.

Coercion pair_of_interval T (I : interval T) : itv_bound T * itv_bound T :=
  let: Interval b1 b2 := I in (b1, b2).

Import Order.TTheory GRing.Theory Num.Theory.

Section itv_simp.
Variables (d : unit) (T : porderType d).
Implicit Types (x y : T) (b : bool).

Lemma ltBSide x y b b' :
  ((BSide b x < BSide b' y) = (x < y ?<= if b && ~~ b'))%O.
d: unit
T: porderType d
x, y: T
b, b': bool
(BSide b x < BSide b' y)%O =
(x < y ?<= if b && ~~ b')%O
Proof.
5c by []. Qed.

Lemma leBSide x y b b' :
  ((BSide b x <= BSide b' y) = (x < y ?<= if b' ==> b))%O.
5e
(BSide b x <= BSide b' y)%O =
(x < y ?<= if b' ==> b)%O
Proof.
66 by []. Qed.

Definition lteBSide := (ltBSide, leBSide).

Let BLeft_ltE x y b : (BSide b x < BLeft y)%O = (x < y)%O.
5f
60
61
b: bool
(BSide b x < BLeft y)%O = (x < y)%O
Proof.
6b by case: b. Qed.
Let BRight_leE x y b : (BSide b x <= BRight y)%O = (x <= y)%O.
5f
60
BLeft_ltE: forall x y b,
(BSide b x < BLeft y)%O = (x < y)%O
61
6e
(BSide b x <= BRight y)%O = (x <= y)%O
Proof.
72 by case: b. Qed.
Let BRight_BLeft_leE x y : (BRight x <= BLeft y)%O = (x < y)%O.
5f
60
75
BRight_leE: forall x y b,
(BSide b x <= BRight y)%O = (x <= y)%O
61
(BRight x <= BLeft y)%O = (x < y)%O
Proof.
79 by []. Qed.
Let BLeft_BRight_ltE x y : (BLeft x < BRight y)%O = (x <= y)%O.
5f
60
75
7c
BRight_BLeft_leE: forall x y,
(BRight x <= BLeft y)%O = (x < y)%O
61
(BLeft x < BRight y)%O = (x <= y)%O
Proof.
80 by []. Qed.
Let BRight_BSide_ltE x y b : (BRight x < BSide b y)%O = (x < y)%O.
5f
60
75
7c
83
BLeft_BRight_ltE: forall x y,
(BLeft x < BRight y)%O = (x <= y)%O
61
6e
(BRight x < BSide b y)%O = (x < y)%O
Proof.
87 by case: b. Qed.
Let BLeft_BSide_leE x y b : (BLeft x <= BSide b y)%O = (x <= y)%O.
5f
60
75
7c
83
8a
BRight_BSide_ltE: forall x y b,
(BRight x < BSide b y)%O =
(x < y)%O
61
6e
(BLeft x <= BSide b y)%O = (x <= y)%O
Proof.
8e by case: b. Qed.
Let BSide_ltE x y b : (BSide b x < BSide b y)%O = (x < y)%O.
5f
60
75
7c
83
8a
91
BLeft_BSide_leE: forall x y b,
(BLeft x <= BSide b y)%O =
(x <= y)%O
61
6e
(BSide b x < BSide b y)%O = (x < y)%O
Proof.
95 by case: b. Qed.
Let BSide_leE x y b : (BSide b x <= BSide b y)%O = (x <= y)%O.
5f
60
75
7c
83
8a
91
98
BSide_ltE: forall x y b,
(BSide b x < BSide b y)%O = (x < y)%O
61
6e
(BSide b x <= BSide b y)%O = (x <= y)%O
Proof.
9c by case: b. Qed.
Let BInfty_leE a : (a <= BInfty T false)%O.
5f
60
75
7c
83
8a
91
98
9f
BSide_leE: forall x y b,
(BSide b x <= BSide b y)%O = (x <= y)%O
a: itv_bound_porderType T
(a <= +oo)%O Proof.
a3 by case: a => [[] a|[]]. Qed.
Let BInfty_geE a : (BInfty T true <= a)%O.
5f
60
75
7c
83
8a
91
98
9f
a6
BInfty_leE: forall a : itv_bound_porderType T,
(a <= +oo)%O
a7
(-oo <= a)%O Proof.
ab by case: a => [[] a|[]]. Qed.
Let BInfty_le_eqE a : (BInfty T false <= a)%O = (a == BInfty T false).
5f
60
75
7c
83
8a
91
98
9f
a6
ae
BInfty_geE: forall a : itv_bound_porderType T,
(-oo <= a)%O
a7
(+oo <= a)%O = (a == +oo%O)
Proof.
b2 by case: a => [[] a|[]]. Qed.
Let BInfty_ge_eqE a : (a <= BInfty T true)%O = (a == BInfty T true).
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
BInfty_le_eqE: forall a : itv_bound_porderType T,
(+oo <= a)%O = (a == +oo%O)
a7
(a <= -oo)%O = (a == -oo%O)
Proof.
b9 by case: a => [[] a|[]]. Qed.
Let BInfty_ltE a : (a < BInfty T false)%O = (a != BInfty T false).
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
BInfty_ge_eqE: forall a : itv_bound_porderType T,
(a <= -oo)%O = (a == -oo%O)
a7
(a < +oo)%O = (a != +oo%O)
Proof.
c0 by case: a => [[] a|[]]. Qed.
Let BInfty_gtE a : (BInfty T true < a)%O = (a != BInfty T true).
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
BInfty_ltE: forall a : itv_bound_porderType T,
(a < +oo)%O = (a != +oo%O)
a7
(-oo < a)%O = (a != -oo%O)
Proof.
c7 by case: a => [[] a|[]]. Qed.
Let BInfty_ltF a : (BInfty T false < a)%O = false.
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
BInfty_gtE: forall a : itv_bound_porderType T,
(-oo < a)%O = (a != -oo%O)
a7
(+oo < a)%O = false
Proof.
ce by case: a => [[] a|[]]. Qed.
Let BInfty_gtF a : (a < BInfty T true)%O = false.
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
d1
BInfty_ltF: forall a : itv_bound_porderType T,
(+oo < a)%O = false
a7
(a < -oo)%O = false
Proof.
d5 by case: a => [[] a|[]]. Qed.
Let BInfty_BInfty_ltE : (BInfty T true < BInfty T false)%O.
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
d1
d8
BInfty_gtF: forall a : itv_bound_porderType T,
(a < -oo)%O = false
(-oo < +oo)%O Proof.
dc by []. Qed.

Lemma ltBRight_leBLeft (a : itv_bound T) (r : T) :
  (a < BRight r)%O = (a <= BLeft r)%O.
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
d1
d8
df
BInfty_BInfty_ltE: (-oo < +oo)%O
a: itv_bound T
r: T
(a < BRight r)%O = (a <= BLeft r)%O
Proof.
e3 by move: a => [[] a|[]]. Qed.
Lemma leBRight_ltBLeft (a : itv_bound T) (r : T) :
  (BRight r <= a)%O = (BLeft r < a)%O.
e5
(BRight r <= a)%O = (BLeft r < a)%O
Proof.
ec by move: a => [[] a|[]]. Qed.

Definition bnd_simp := (BLeft_ltE, BRight_leE,
  BRight_BLeft_leE, BLeft_BRight_ltE,
  BRight_BSide_ltE, BLeft_BSide_leE, BSide_ltE, BSide_leE,
  BInfty_leE, BInfty_geE, BInfty_BInfty_ltE,
  BInfty_le_eqE, BInfty_ge_eqE, BInfty_ltE, BInfty_gtE, BInfty_ltF, BInfty_gtF,
  @lexx _ T, @ltxx _ T, @eqxx T).

Lemma itv_splitU1 (a : itv_bound T) (x : T) : (a <= BLeft x)%O ->
  Interval a (BRight x) =i [predU1 x & Interval a (BLeft x)].
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
d1
d8
df
e6
e7
x: T
(a <= BLeft x)%O ->
Interval a (BRight x)
  =i [predU1 x & Interval a (BLeft x)]
Proof.
f1
move=> ax z; rewrite !inE/= !subitvE ?bnd_simp//= lt_neqAle.
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
d1
d8
df
e6
e7
f4
ax: (a <= BLeft x)%O
z: T
(a <= BLeft z)%O && (z <= x)%O =
(z == x) || [&& (a <= BLeft z)%O, z != x & (z <= x)%O]
by case: (eqVneq z x) => [->|]//=; rewrite lexx ax.
Qed.

Lemma itv_split1U (a : itv_bound T) (x : T) : (BRight x <= a)%O ->
  Interval (BLeft x) a =i [predU1 x & Interval (BRight x) a].
f3
(BRight x <= a)%O ->
Interval (BLeft x) a
  =i [predU1 x & Interval (BRight x) a]
Proof.
ff
move=> ax z; rewrite !inE/= !subitvE ?bnd_simp//= lt_neqAle.
5f
60
75
7c
83
8a
91
98
9f
a6
ae
b5
bc
c3
ca
d1
d8
df
e6
e7
f4
ax: (BRight x <= a)%O
fc
(x <= z)%O && (BRight z <= a)%O =
(z == x)
|| (x != z) && (x <= z)%O && (BRight z <= a)%O
by case: (eqVneq z x) => [->|]//=; rewrite lexx ax.
Qed.

End itv_simp.

Definition miditv (R : numDomainType) (i : interval R) : R :=
  match i with
  | Interval (BSide _ a) (BSide _ b) => (a + b) / 2%:R
  | Interval -oo%O (BSide _ b) => b - 1
  | Interval (BSide _ a) +oo%O => a + 1
  | Interval -oo%O +oo%O => 0
  | _ => 0
  end.

Section miditv_lemmas.
Variable R : numFieldType.
Implicit Types i : interval R.

Lemma mem_miditv i : (i.1 < i.2)%O -> miditv i \in i.
R: numFieldType
i: interval R
(i.1 < i.2)%O -> miditv i \in i
Proof.
10a
move: i => [[ba a|[]] [bb b|[]]] //= ab; first exact: mid_in_itv.
10d
ba: bool
a: R
ab: (BSide ba a < +oo)%O
(a + 1)%R \in Interval (BSide ba a) +oo%O
10d
bb: bool
b: R
ab: (-oo < BSide bb b)%O
(b - 1)%R \in Interval -oo%O (BSide bb b)
  by rewrite !in_itv -lteif_subl_addl subrr lteif01.
11b
11f
by rewrite !in_itv lteif_subl_addr -lteif_subl_addl subrr lteif01.
Qed.

Lemma miditv_le_left i b : (i.1 < i.2)%O -> (BSide b (miditv i) <= i.2)%O.
10d
10e
6e
(i.1 < i.2)%O -> (BSide b (miditv i) <= i.2)%O
Proof.
124
case: i => [x y] lti; have := mem_miditv lti; rewrite inE => /andP[_ ].
10d
6e
x, y: itv_bound R
lti: ((Interval x y).1 < (Interval x y).2)%O
(BRight (miditv (Interval x y)) <= y)%O ->
(BSide b (miditv (Interval x y)) <= (Interval x y).2)%O
by apply: le_trans; rewrite !bnd_simp.
Qed.

Lemma miditv_ge_right i b : (i.1 < i.2)%O -> (i.1 <= BSide b (miditv i))%O.
126
(i.1 < i.2)%O -> (i.1 <= BSide b (miditv i))%O
Proof.
131
case: i => [x y] lti; have := mem_miditv lti; rewrite inE => /andP[+ _].
12c
(x <= BLeft (miditv (Interval x y)))%O ->
((Interval x y).1 <= BSide b (miditv (Interval x y)))%O
by move=> /le_trans; apply; rewrite !bnd_simp.
Qed.

End miditv_lemmas.

Section itv_porderType.
Variables (d : unit) (T : orderType d).
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).

Lemma predC_itvl a : [predC Interval -oo%O a] =i Interval a +oo%O.
5f
T: orderType d
e7
[predC Interval -oo%O a] =i Interval a +oo%O
Proof.
13a
case: a => [b x|[]//] y.
5f
13d
6e
61
(y \in [predC Interval -oo%O (BSide b x)]) =
(y \in Interval (BSide b x) +oo%O)
by rewrite !inE !subitvE/= bnd_simp andbT !lteBSide/= lteifNE negbK.
Qed.

Lemma predC_itvr a : [predC Interval a +oo%O] =i Interval -oo%O a.
13c
[predC Interval a +oo%O] =i Interval -oo%O a
Proof.
146 by move=> y; rewrite inE/= -predC_itvl negbK. Qed.

Lemma predC_itv i : [predC i] =i [predU Interval -oo%O i.1 & Interval i.2 +oo%O].
5f
13d
i: interval T
[predC i]
  =i [predU Interval -oo%O i.1 & Interval i.2 +oo%O]
Proof.
14b
case: i => [a a']; move=> x; rewrite inE/= itv_splitI negb_and.
5f
13d
a, a': itv_bound T
f4
(x \notin Interval a +oo%O)
|| (x \notin Interval -oo%O a') =
(x \in [predU Interval -oo%O a & Interval a' +oo%O])
by symmetry; rewrite inE/= -predC_itvl -predC_itvr.
Qed.

End itv_porderType.

Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I -> R) :
  (forall i, P i -> F i <= 0)%R -> (\sum_(i <- r | P i) F i <= 0)%R.
R: numDomainType
I: Type
r: seq I
P: pred I
F: I -> R
(forall i : I, P i -> (F i <= 0)%R) ->
(\sum_(i <- r | P i) F i <= 0)%R
Proof.
158 by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_naddl/F0. Qed.

Lemma enum_ord0 : enum 'I_0 = [::].
enum 'I_0 = [::]
Proof.
163 by apply/eqP; rewrite -size_eq0 size_enum_ord. Qed.

Lemma enum_ordSr n : enum 'I_n.+1 =
  rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max.
n: nat
enum 'I_n.+1 =
rcons [seq widen_ord (leqnSn n) i | i <- enum 'I_n]
  ord_max
Proof.
168
apply: (inj_map val_inj); rewrite val_enum_ord.
16a
iota 0 n.+1 =
[seq val i
   | i <- rcons
            [seq widen_ord (leqnSn n) i
               | i <- enum 'I_n] ord_max]
rewrite -[in iota _  _]addn1 iotaD/= cats1 map_rcons; congr (rcons _ _).
16a
iota 0 n =
[seq i
   | i <- [seq widen_ord (leqnSn n) i
             | i <- enum 'I_n]]
by rewrite -map_comp/= (@eq_map _ _ _ val) ?val_enum_ord.
Qed.

Lemma obindEapp {aT rT} (f : aT -> option rT) : obind f = oapp f None.
aT, rT: Type
f: aT -> option rT
obind f = oapp f None
Proof.
177 by []. Qed.

Lemma omapEbind {aT rT} (f : aT -> rT) : omap f = obind (olift f).
17a
f
omap f = obind (olift f)
Proof.
17f by []. Qed.

Lemma omapEapp {aT rT} (f : aT -> rT) : omap f = oapp (olift f) None.
181
omap f = oapp (olift f) None
Proof.
185 by []. Qed.

Lemma oappEmap {aT rT} (f : aT -> rT) (y0 : rT) x :
  oapp f y0 x = odflt y0 (omap f x).
17a
f
y0: rT
x: option aT
oapp f y0 x = odflt y0 (omap f x)
Proof.
18a by case: x. Qed.

Lemma omap_comp aT rT sT (f : aT -> rT) (g : rT -> sT) :
  omap (g \o f) =1 omap g \o omap f.
17
omap (g \o f) =1 omap g \o omap f
Proof.
192 by case. Qed.

Lemma oapp_comp_f {aT rT sT} (f : aT -> rT) (g : rT -> sT) (x : rT) :
  oapp (g \o f) (g x) =1 g \o oapp f x.
e
f
10
x: rT
oapp (g \o f) (g x) =1 g \o oapp f x
Proof.
197 by case. Qed.

Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
    [f : B -> A] [h : C -> B]
    [f' : A -> B] [h' : B -> C] :
  {homo h : x / x \in D' >-> x \in D} ->
  {in D, cancel f f'} -> {in D', cancel h h'} ->
  {in D', cancel (f \o h) (h' \o f')}.
38
39
3a
1f
h: C -> B
3d
3e
{homo h : x / x \in D' >-> x \in D} ->
{in D, cancel f f'} ->
{in D', cancel h h'} ->
{in D', cancel (f \o h) (h' \o f')}
Proof.
19e by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed.

Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) :
  {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} ->
  {in Q &, injective (f \o h)}.
38
1f
1a1
P: pred B
Q: pred C
{in P &, injective f} ->
{in Q &, injective h} ->
{homo h : x / Q x >-> P x} ->
{in Q &, injective (f \o h)}
Proof.
1a5
by move=> Pf Qh QP x y xQ yQ xy; apply Qh => //; apply Pf => //; apply QP.
Qed.

Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
    [f : B -> A] [h : C -> B]
    [f' : A -> option B] [h' : B -> option C] :
  {homo h : x / x \in D' >-> x \in D} ->
  {in D, pcancel f f'} -> {in D', pcancel h h'} ->
  {in D', pcancel (f \o h) (obind h' \o f')}.
38
39
3a
1f
1a1
f': A -> option B
h': B -> option C
{homo h : x / x \in D' >-> x \in D} ->
{in D, pcancel f f'} ->
{in D', pcancel h h'} ->
{in D', pcancel (f \o h) (obind h' \o f')}
Proof.
1ad by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed.

Lemma ocan_comp [A B C : Type] [f : B -> option A] [h : C -> option B]
    [f' : A -> B] [h' : B -> C] :
  ocancel f f' -> ocancel h h' -> ocancel (obind f \o h) (h' \o f').
38
3b
3c
3d
3e
ocancel f f' ->
ocancel h h' -> ocancel (obind f \o h) (h' \o f')
Proof.
1b5
move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=.
38
3b
3c
3d
3e
fK: ocancel f f'
hK: ocancel h h'
48
4a
4b
4c
by rewrite -[b in RHS]fK; case: (f b) => //=; have := hK c; rewrite hcE.
Qed.

Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2.
55
b1 = b2 -> b1 -> b2
Proof.
1c1 by move->. Qed.

Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x).
Notation "f \max g" := (max_fun f g) : ring_scope.
Arguments max_fun {T R} _ _ _ /.

Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R.
15b
r: R
(0 < r)%R -> (- r < r)%R
Proof.
1c6 by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed.

Lemma le_le_trans {disp : unit} {T : porderType disp} (x y z t : T) :
  (z <= x)%O -> (y <= t)%O -> (x <= y)%O -> (z <= t)%O.
disp: unit
T: porderType disp
x, y, z, t: T
(z <= x)%O -> (y <= t)%O -> (x <= y)%O -> (z <= t)%O
Proof.
1cd by move=> + /(le_trans _)/[apply]; apply: le_trans. Qed.

Notation eqLHS := (X in (X == _))%pattern.
Notation eqRHS := (X in (_ == X))%pattern.
Notation leLHS := (X in (X <= _)%O)%pattern.
Notation leRHS := (X in (_ <= X)%O)%pattern.
Notation ltLHS := (X in (X < _)%O)%pattern.
Notation ltRHS := (X in (_ < X)%O)%pattern.
Inductive boxed T := Box of T.

Lemma eq_bigl_supp [R : eqType] [idx : R] [op : Monoid.law idx] [I : Type]
  [r : seq I] [P1 : pred I] (P2 : pred I) (F : I -> R) :
  {in [pred x | F x != idx], P1 =1 P2} ->
  \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.
R: eqType
idx: R
op: Monoid.law idx
15c
15d
P1, P2: pred I
15f
{in [pred x | F x != idx], P1 =1 P2} ->
\big[op/idx]_(i <- r | P1 i) F i =
\big[op/idx]_(i <- r | P2 i) F i
Proof.
1d6
move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _.
1d9
1da
1db
15c
15d
1dc
15f
P12: {in [pred x | F x != idx], P1 =1 P2}
i: I
(if P1 i then F i else idx) =
(if P2 i then F i else idx)
by case: (eqVneq (F i) idx) => [->|/P12->]; rewrite ?if_same.
Qed.

Lemma perm_big_supp_cond [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType]
  [r s : seq I] [P : pred I] (F : I -> R) :
  perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] ->
  \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i.
1d9
1da
op: Monoid.com_law idx
I: eqType
r, s: seq I
15e
15f
perm_eq [seq i <- r | P i & F i != idx]
  [seq i <- s | P i & F i != idx] ->
\big[op/idx]_(i <- r | P i) F i =
\big[op/idx]_(i <- s | P i) F i
Proof.
1e7
move=> prs; rewrite !(bigID [pred i | F i == idx] P F)/=.
1d9
1da
1ea
1eb
1ec
15e
15f
prs: perm_eq [seq i <- r | P i & F i != idx] [seq i <- s | P i & F i != idx]
op (\big[op/idx]_(i <- r | P i && (F i == idx)) F i)
  (\big[op/idx]_(i <- r | P i && (F i != idx)) F i) =
op (\big[op/idx]_(i <- s | P i && (F i == idx)) F i)
  (\big[op/idx]_(i <- s | P i && (F i != idx)) F i)
rewrite big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->].
1f2
\big[op/idx]_(i <- r | P i && (F i != idx)) F i =
op (\big[op/idx]_(i <- s | P i && (F i == idx)) F i)
  (\big[op/idx]_(i <- s | P i && (F i != idx)) F i)
rewrite [in RHS]big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->].
1f2
\big[op/idx]_(i <- r | P i && (F i != idx)) F i =
\big[op/idx]_(i <- s | P i && (F i != idx)) F i
by rewrite -[in LHS]big_filter -[in RHS]big_filter; apply perm_big.
Qed.

Lemma perm_big_supp [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType]
  [r s : seq I] [P : pred I] (F : I -> R) :
  perm_eq [seq i <- r | (F i != idx)] [seq i <- s | (F i != idx)] ->
  \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i.
1e9
perm_eq [seq i <- r | F i != idx]
  [seq i <- s | F i != idx] ->
\big[op/idx]_(i <- r | P i) F i =
\big[op/idx]_(i <- s | P i) F i
Proof.
1fe
by move=> ?; apply: perm_big_supp_cond; rewrite !filter_predI perm_filter.
Qed.

Local Open Scope order_scope.
Local Open Scope ring_scope.
Import GRing.Theory Order.TTheory.

Lemma mulr_ge0_gt0 (R : numDomainType) (x y : R) : 0 <= x -> 0 <= y ->
  (0 < x * y) = (0 < x) && (0 < y).
15b
x, y: R
0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y)
Proof.
203
rewrite le_eqVlt => /predU1P[<-|x0]; first by rewrite mul0r ltxx.
15b
206
x0: 0 < x
0 <= y -> (0 < x * y) = (0 < x) && (0 < y)
rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite mulr0 ltxx andbC.
15b
206
20d
y0: 0 < y
(0 < x * y) = (0 < x) && (0 < y)
by apply/idP/andP=> [|_]; rewrite pmulr_rgt0.
Qed.

Section lt_le_gt_ge.
Variable (R : numFieldType).
Implicit Types x y z a b : R.

Lemma splitr x : x = x / 2%:R + x / 2%:R.
10d
x: R
x = x / 2 + x / 2
Proof.
216 by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed.

Lemma ler_addgt0Pr x y : reflect (forall e, e > 0 -> x <= y + e) (x <= y).
10d
206
reflect (forall e : R, 0 < e -> x <= y + e) (x <= y)
Proof.
21d
apply/(iffP idP)=> [lexy e e_gt0 | lexye]; first by rewrite ler_paddr// ltW.
10d
206
lexye: forall e : R, 0 < e -> x <= y + e
x <= y
have [||ltyx]// := comparable_leP.
225
x >=< y
10d
206
226
ltyx: y < x
false
  rewrite (@comparabler_trans _ (y + 1))// /Order.comparable ?lexye ?ltr01//.
225
(y + 1 <= y) || (y <= y + 1)
22c
  by rewrite ler_addl ler01 orbT.
22e
230
have /midf_lt [_] := ltyx; rewrite le_gtF//.
22e
x <= (y + x) / 2
rewrite -(@addrK _ y y) addrAC -addrA 2!mulrDl -splitr lexye//.
22e
0 < (x - y) / 2
by rewrite divr_gt0// ?ltr0n// subr_gt0.
Qed.

Lemma ler_addgt0Pl x y : reflect (forall e, e > 0 -> x <= e + y) (x <= y).
21f
reflect (forall e : R, 0 < e -> x <= e + y) (x <= y)
Proof.
241
by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC.
Qed.

Lemma in_segment_addgt0Pr x y z :
  reflect (forall e, e > 0 -> y \in `[x - e, z + e]) (y \in `[x, z]).
10d
x, y, z: R
reflect
  (forall e : R, 0 < e -> y \in `[(x - e), (z + e)])
  (y \in `[x, z])
Proof.
246
apply/(iffP idP)=> [xyz e /[dup] e_gt0 /ltW e_ge0 | xyz_e].
10d
249
xyz: y \in `[x, z]
e: R
e_gt0: 0 < e
e_ge0: 0 <= e
y \in `[(x - e), (z + e)]
10d
249
xyz_e: forall e : R,
0 < e -> y \in `[(x - e), (z + e)]
y \in `[x, z]
  by rewrite in_itv /= ler_subl_addr !ler_paddr// (itvP xyz).
257
259
by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e;
   rewrite in_itv /= ler_subl_addr => /andP [].
Qed.

Lemma in_segment_addgt0Pl x y z :
  reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]).
248
reflect
  (forall e : R, 0 < e -> y \in `[(- e + x), (e + z)])
  (y \in `[x, z])
Proof.
25e
apply/(equivP (in_segment_addgt0Pr x y z)).
248
(forall e : R, 0 < e -> y \in `[(x - e), (z + e)]) <->
(forall e : R, 0 < e -> y \in `[(- e + x), (e + z)])
by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC.
Qed.

Lemma lt_le a b : (forall x, x < a -> x < b) -> a <= b.
10d
a, b: R
(forall x, x < a -> x < b) -> a <= b
Proof.
267
move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -ler_subl_addr ltW//.
10d
26a
ab: forall x, x < a -> x < b
251
252
a - e < b
by rewrite ab // ltr_subl_addr -ltr_subl_addl subrr.
Qed.

Lemma gt_ge a b : (forall x, b < x -> a < x) -> a <= b.
269
(forall x, b < x -> a < x) -> a <= b
Proof.
274
move=> ab; apply/ler_addgt0Pr => e e_gt0.
10d
26a
ab: forall x, b < x -> a < x
251
252
a <= b + e
by rewrite ltW// ab// -ltr_subl_addl subrr.
Qed.

End lt_le_gt_ge.

Lemma itvxx d (T : porderType d) (x : T) : `[x, x] =i pred1 x.
5f
60
f4
`[x, x] =i pred1 x
Proof.
27f by move=> y; rewrite in_itv/= -eq_le eq_sym. Qed.

Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).
5f
60
61
reflect (y = x) (y \in `[x, x])
Proof.
285 by rewrite itvxx; apply/eqP. Qed.

Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ <= `[a, b]}.
5f
60
a, b: T
{subset `]a, b[ <= `[a, b]}
Proof.
28b by apply: subitvP; rewrite subitvE !bound_lexx. Qed.

(**********************************)
(* End of MathComp 1.15 additions *)
(**********************************)

Reserved Notation "`1- r" (format "`1- r", at level 2).
Reserved Notation "f \^-1" (at level 3, format "f \^-1").

Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R.
R: ringType
16b
n%:R + 1 = n.+1%:R
Proof.
292 by rewrite GRing.mulrSr. Qed.

Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R.
294
1 + n%:R = n.+1%:R
Proof.
299 by rewrite GRing.mulrS. Qed.

(* To be backported to finmap *)

Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
    (f : X -> nat) : A != fset0 ->
  (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat.
X: choiceType
A: {fset X}
f: X -> nat
A != fset0 ->
exists i : X,
  i \in A /\ (forall j : X, j \in A -> (f j <= f i)%N)
Proof.
29e
move=> /fset0Pn[x Ax].
2a1
2a2
2a3
x: X
Ax: x \in A
exists i : X,
  i \in A /\ (forall j : X, j \in A -> (f j <= f i)%N)
have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT.
2a1
2a2
2a3
2aa
2ab
y: A
mf: forall f0 : A, (f (fsval f0) <= f (fsval y))%N
2ac
exists (val y); split; first exact: valP.
2b0
forall j : X, j \in A -> (f j <= f (val y))%N
by move=> z Az; have := mf [` Az]%fset.
Qed.

Lemma image_nat_maximum n (f : nat -> nat) :
  (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N.
16b
f: nat -> nat
exists i : nat,
  (i <= n)%N /\
  (forall j : nat, (j <= n)%N -> (f j <= f i)%N)
Proof.
2b8
have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT.
16b
2bb
i: ordinal_finType n.+1
mf: forall s : ordinal_finType n.+1, geq (f i) (f s)
2bc
by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn).
Qed.

Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
  #|` A| = (\sum_(i <- A) 1)%N.
T: choiceType
A: {fset T}
#|` A| = (\sum_(i <- A) 1)%N
Proof.
2c5 by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.

Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.

(*******************************)
(* MathComp > 1.15.0 additions *)
(*******************************)

Section bigminr_maxr.
Import Num.Def.

Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I -> R) x :
  \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i.
R: realDomainType
15c
15d
15e
15f
219
\big[minr/x]_(i <- r | P i) F i =
- (\big[maxr/(- x)]_(i <- r | P i) - F i)
Proof.
2cd
by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK.
Qed.
End bigminr_maxr.

Section SemiGroupProperties.
Variables (R : Type) (op : R -> R -> R).
Hypothesis opA : associative op.

(* Convert an AC op : R -> R -> R to a com_law on option R *)
Definition AC_subdef of associative op & commutative op :=
  fun x => oapp (fun y => Some (oapp (op^~ y) y x)) x.
Definition oAC := nosimpl AC_subdef.

Hypothesis opC : commutative op.
Let opCA : left_commutative op.
R: Type
op: R -> R -> R
opA: associative op
opC: commutative op
left_commutative op Proof.
2d4 by move=> x *; rewrite !opA (opC x). Qed.
Let opAC : right_commutative op.
2d7
2d8
2d9
2da
opCA: left_commutative op
right_commutative op
Proof.
2de by move=> *; rewrite -!opA [X in op _ X]opC. Qed.

Hypothesis opyy : idempotent op.

Local Notation oop := (oAC opA opC).

Lemma opACE x y : oop (Some x) (Some y) = some (op x y).
2d7
2d8
2d9
2da
2e1
opAC: right_commutative op
opyy: idempotent op
206
oop (Some x) (Some y) = Some (op x y) Proof.
2e5 by []. Qed.

Lemma oopA_subdef : associative oop.
2d7
2d8
2d9
2da
2e1
2e8
2e9
associative oop
Proof.
2ed by move=> [x|] [y|] [z|]//; rewrite /oAC/= opA. Qed.

Lemma oopx1_subdef : left_id None oop.
2ef
left_id None oop Proof.
2f3 by case. Qed.
Lemma oop1x_subdef : right_id None oop.
2ef
right_id None oop Proof.
2f8 by []. Qed.

Lemma oopC_subdef : commutative oop.
2ef
commutative oop
Proof.
2fd by move=> [x|] [y|]//; rewrite /oAC/= opC. Qed.

Canonical opAC_law := Monoid.Law oopA_subdef oopx1_subdef oop1x_subdef.
Canonical opAC_com_law := Monoid.ComLaw oopC_subdef.

Context [x : R].

Lemma some_big_AC [I : Type] r P (F : I -> R) :
  Some (\big[op/x]_(i <- r | P i) F i) =
  oop (\big[oop/None]_(i <- r | P i) Some (F i)) (Some x).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
15c
15d
P: I -> bool
15f
Some (\big[op/x]_(i <- r | P i) F i) =
oop (\big[oop/None]_(i <- r | P i) Some (F i))
  (Some x)
Proof.
302 by elim/big_rec2 : _ => //= i [y|] _ Pi [] -> //=; rewrite opA. Qed.

Lemma big_ACE [I : Type] r P (F : I -> R) :
  \big[op/x]_(i <- r | P i) F i =
  odflt x (oop (\big[oop/None]_(i <- r | P i) Some (F i)) (Some x)).
304
\big[op/x]_(i <- r | P i) F i =
odflt x
  (oop (\big[oop/None]_(i <- r | P i) Some (F i))
     (Some x))
Proof.
309 by apply: Some_inj; rewrite some_big_AC. Qed.

Lemma big_undup_AC [I : eqType] r P (F : I -> R) (opK : idempotent op) :
  \big[op/x]_(i <- undup r | P i) F i = \big[op/x]_(i <- r | P i) F i.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
1eb
15d
305
15f
opK: idempotent op
\big[op/x]_(i <- undup r | P i) F i =
\big[op/x]_(i <- r | P i) F i
Proof.
30e by rewrite !big_ACE !big_undup//; case=> //= ?; rewrite /oAC/= opK. Qed.

Lemma perm_big_AC [I : eqType] [r] s [P : pred I] [F : I -> R] :
 perm_eq r s -> \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- s | P i) F i.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
1eb
1ec
15e
15f
perm_eq r s ->
\big[op/x]_(i <- r | P i) F i =
\big[op/x]_(i <- s | P i) F i
Proof.
315 by rewrite !big_ACE => /(@perm_big _ _)->. Qed.

Section Id.
Hypothesis opxx : op x x = x.

Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
opxx: op x x = x
15c
15d
305
\big[op/x]_(i <- r | P i) x = x
Proof.
31b by elim/big_ind : _ => // _ _ -> ->. Qed.

Lemma big_id_idem I (r : seq I) P F :
  op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
31e
15c
15d
305
15f
op (\big[op/x]_(i <- r | P i) F i) x =
\big[op/x]_(i <- r | P i) F i
Proof.
322 by elim/big_rec : _ => // ? ? ?; rewrite -opA => ->. Qed.

Lemma big_mkcond_idem I r (P : pred I) F :
  \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
31e
15c
15d
15e
15f
\big[op/x]_(i <- r | P i) F i =
\big[op/x]_(i <- r) (if P i then F i else x)
Proof.
328
elim: r => [|i r]; rewrite ?(big_nil, big_cons)//.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
31e
15c
15e
15f
1e4
15d
\big[op/x]_(i <- r | P i) F i =
\big[op/x]_(i <- r) (if P i then F i else x) ->
(if P i
 then op (F i) (\big[op/x]_(j <- r | P j) F j)
 else \big[op/x]_(j <- r | P j) F j) =
op (if P i then F i else x)
  (\big[op/x]_(j <- r) (if P j then F j else x))
by case: ifPn => Pi ->//; rewrite -[in LHS]big_id_idem.
Qed.

Lemma big_split_idem I r (P : pred I) F1 F2 :
  \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) =
    op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
31e
15c
15d
15e
F1, F2: I -> R
\big[op/x]_(i <- r | P i) op (F1 i) (F2 i) =
op (\big[op/x]_(i <- r | P i) F1 i)
  (\big[op/x]_(i <- r | P i) F2 i)
Proof.
333 by elim/big_rec3 : _ => [//|i ? ? _ _ ->]; rewrite // opCA -!opA opCA. Qed.

Lemma big_id_idem_AC I (r : seq I) P F :
  \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i.
324
\big[op/x]_(i <- r | P i) op (F i) x =
\big[op/x]_(i <- r | P i) F i
Proof.
33a by rewrite big_split_idem big_const_idem ?big_id_idem. Qed.

Lemma bigID_idem I r (a P : pred I) F :
  \big[op/x]_(i <- r | P i) F i =
    op (\big[op/x]_(i <- r | P i && a i) F i)
       (\big[op/x]_(i <- r | P i && ~~ a i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
31e
15c
15d
a, P: pred I
15f
\big[op/x]_(i <- r | P i) F i =
op (\big[op/x]_(i <- r | P i && a i) F i)
  (\big[op/x]_(i <- r | P i && ~~ a i) F i)
Proof.
33f
rewrite -big_id_idem_AC big_mkcond_idem !(big_mkcond_idem _ _ F) -big_split_idem.
341
\big[op/x]_(i <- r) (if P i then op (F i) x else x) =
\big[op/x]_(i <- r)
   op (if P i && a i then F i else x)
     (if P i && ~~ a i then F i else x)
by apply: eq_bigr => i; case: ifPn => //=; case: ifPn.
Qed.

End Id.

Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r ->
  \big[op/x]_(y <- r | P y) F y =
    if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y)
           else \big[op/x]_(y <- rem z r | P y) F y.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
1eb
15d
z: I
15e
15f
z \in r ->
\big[op/x]_(y <- r | P y) F y =
(if P z
 then op (F z) (\big[op/x]_(y <- rem z r | P y) F y)
 else \big[op/x]_(y <- rem z r | P y) F y)
Proof.
34a
by move=> /[!big_ACE] /(big_rem _)->//; case: ifP; case: (bigop _ _ _) => /=.
Qed.

Lemma bigD1_AC (I : finType) j (P : pred I) F : P j ->
  \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
I: finType
j: I
15e
15f
P j ->
\big[op/x]_(i | P i) F i =
op (F j) (\big[op/x]_(i | P i && (i != j)) F i)
Proof.
351 by move=> /[!big_ACE] /(bigD1 _)->; case: (bigop _ _) => /=. Qed.

Variable le : rel R.
Hypothesis le_refl : reflexive le.
Hypothesis op_incr : forall x y, le x (op x y).

Lemma sub_big I [s] (P P' : {pred I}) (F : I -> R) : (forall i, P i -> P' i) ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
le: rel R
le_refl: reflexive le
op_incr: forall x y : R, le x (op x y)
15c
s: seq I
P, P': {pred I}
15f
(forall i : I, P i -> P' i) ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s | P' i) F i)
Proof.
359
move=> PP'; rewrite !big_ACE (bigID P P')/=.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
15c
35f
360
15f
PP': forall i : I, P i -> P' i
le
  (oapp (op^~ x) x
     (\big[oop/None]_(i <- s | P i) Some (F i)))
  (oapp (op^~ x) x
     (oop
        (\big[oop/None]_(i <- s | P' i && P i)
            Some (F i))
        (\big[oop/None]_(i <- s | P' i && ~~ P i)
            Some (F i))))
under [in X in le _ X]eq_bigl do rewrite (andb_idl (PP' _)).
366
le
  (oapp (op^~ x) x
     (\big[oop/None]_(i <- s | P i) Some (F i)))
  (oapp (op^~ x) x
     (oop (\big[oop/None]_(i <- s | P i) Some (F i))
        (\big[oop/None]_(i <- s | P' i && ~~ P i)
            Some (F i))))
case: (bigop _ _ _) (bigop _ _ _) => [y|] [z|]//=.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
15c
35f
360
15f
367
y, z: R
le (op z x) (op (op z y) x)
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
15c
35f
360
15f
367
y: R
le x (op y x)
  by rewrite opAC op_incr.
375
377
by rewrite opC op_incr.
Qed.

Lemma sub_big_seq (I : eqType) s s' P (F : I -> R) :
  (forall i, count_mem i s <= count_mem i s')%N ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
s, s': seq I
305
15f
(forall i : I, (count_mem i s <= count_mem i s')%N) ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s' | P i) F i)
Proof.
37c
rewrite !big_ACE => /count_subseqP[_ /subseqP[m sm ->]]/(perm_big _)->.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
37f
305
15f
m: seq bool
sm: size m = size s'
le
  (odflt x
     (oop
        (\big[opAC_com_law/None]_(i <- mask m s' | 
         P i) Some (F i)) (Some x)))
  (odflt x
     (oop (\big[oop/None]_(i <- s' | P i) Some (F i))
        (Some x)))
by rewrite big_mask big_tnth// -!big_ACE sub_big// => j /andP[].
Qed.

Lemma sub_big_seq_cond (I : eqType) s s' P P' (F : I -> R) :
    (forall i, count_mem i (filter P s) <= count_mem i (filter P' s'))%N ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
37f
P, P': pred I
15f
(forall i : I,
 (count_mem i [seq x <- s | P x] <=
  count_mem i [seq x <- s' | P' x])%N) ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s' | P' i) F i)
Proof.
38a by  move=> /(sub_big_seq xpredT F); rewrite !big_filter. Qed.

Lemma uniq_sub_big (I : eqType) s s' P (F : I -> R) : uniq s -> uniq s' ->
    {subset s <= s'} ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P i) F i).
37e
uniq s ->
uniq s' ->
{subset s <= s'} ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s' | P i) F i)
Proof.
391
move=> us us' ss'; rewrite sub_big_seq => // i; rewrite !count_uniq_mem//.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
37f
305
15f
us: uniq s
us': uniq s'
ss': {subset s <= s'}
1e4
((i \in s) <= (i \in s'))%N
by have /implyP := ss' i; case: (_ \in s) (_ \in s') => [] [].
Qed.

Lemma uniq_sub_big_cond (I : eqType) s s' P P' (F : I -> R) :
    uniq (filter P s) -> uniq (filter P' s') ->
    {subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P' i) F i).
38c
uniq [seq x <- s | P x] ->
uniq [seq x <- s' | P' x] ->
{subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s' | P' i) F i)
Proof.
39e by move=> u u' /(uniq_sub_big xpredT F u u'); rewrite !big_filter. Qed.

Lemma sub_big_idem (I : eqType) s s' P (F : I -> R) :
    {subset s <= s'} ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
s, s': seq_predType I
305
15f
{subset s <= s'} ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s' | P i) F i)
Proof.
3a3
move=> ss'; rewrite -big_undup_AC// -[X in le _ X]big_undup_AC//.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
3a6
305
15f
39b
le (\big[op/x]_(i <- undup s | P i) F i)
  (\big[op/x]_(i <- undup s' | P i) F i)
by rewrite uniq_sub_big ?undup_uniq// => i; rewrite !mem_undup; apply: ss'.
Qed.

Lemma sub_big_idem_cond (I : eqType) s s' P P' (F : I -> R) :
    {subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
37f
P, P': I -> bool
15f
{subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s' | P' i) F i)
Proof.
3af by  move=> /(sub_big_idem xpredT F); rewrite !big_filter. Qed.

Lemma sub_in_big [I : eqType] (s : seq I) (P P' : {pred I}) (F : I -> R) :
    {in s, forall i, P i -> P' i} ->
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
35f
360
15f
{in s, forall i : I, P i -> P' i} ->
le (\big[op/x]_(i <- s | P i) F i)
  (\big[op/x]_(i <- s | P' i) F i)
Proof.
3b6
move=> PP'; apply: sub_big_seq_cond => i; rewrite leq_count_subseq//.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
35f
360
15f
PP': {in s, forall i : I, P i -> P' i}
1e4
subseq [seq x <- s | P x] [seq x <- s | P' x]
rewrite subseq_filter filter_subseq andbT; apply/allP => j.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
1eb
35f
360
15f
3bf
i, j: I
j \in [seq x <- s | P x] -> P' j
by rewrite !mem_filter => /andP[/PP'/[apply]->].
Qed.

Lemma le_big_ord n m [P : {pred nat}] [F : nat -> R] : (n <= m)%N ->
  le (\big[op/x]_(i < n | P i) F i) (\big[op/x]_(i < m | P i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
n, m: nat
P: {pred nat}
F: nat -> R
(n <= m)%N ->
le (\big[op/x]_(i < n | P i) F i)
  (\big[op/x]_(i < m | P i) F i)
Proof.
3c8
by move=> nm; rewrite (big_ord_widen_cond m)// sub_big => //= ? /andP[].
Qed.

Lemma subset_big [I : finType] [A A' P : {pred I}] (F : I -> R) :
    A \subset A' ->
  le (\big[op/x]_(i in A | P i) F i) (\big[op/x]_(i in A' | P i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
354
A, A', P: {pred I}
15f
A \subset A' ->
le (\big[op/x]_(i in A | P i) F i)
  (\big[op/x]_(i in A' | P i) F i)
Proof.
3d1
move=> AA'; apply: sub_big => y /andP[yA yP]; apply/andP; split => //.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
354
3d4
15f
AA': A \subset A'
y: I
yA: y \in A
yP: P y
y \in A'
exact: subsetP yA.
Qed.

Lemma subset_big_cond (I : finType) (A A' P P' : {pred I}) (F : I -> R) :
    [set i in A | P i]  \subset [set i in A' | P' i] ->
  le (\big[op/x]_(i in A | P i) F i) (\big[op/x]_(i in A' | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
354
A, A', P, P': {pred I}
15f
[set i in A | P i] \subset [set i in A' | P' i] ->
le (\big[op/x]_(i in A | P i) F i)
  (\big[op/x]_(i in A' | P' i) F i)
Proof.
3e1 by move=> /subsetP AP; apply: sub_big => i; have /[!inE] := AP i. Qed.

Lemma le_big_nat_cond n m n' m' (P P' : {pred nat}) (F : nat -> R) :
    (n' <= n)%N -> (m <= m')%N -> (forall i, (n <= i < m)%N -> P i -> P' i) ->
  le (\big[op/x]_(n <= i < m | P i) F i) (\big[op/x]_(n' <= i < m' | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
n, m, n', m': nat
P, P': {pred nat}
3cd
(n' <= n)%N ->
(m <= m')%N ->
(forall i : nat, (n <= i < m)%N -> P i -> P' i) ->
le (\big[op/x]_(n <= i < m | P i) F i)
  (\big[op/x]_(n' <= i < m' | P' i) F i)
Proof.
3e8
move=> len'n lemm' PP'i; rewrite uniq_sub_big_cond ?filter_uniq ?iota_uniq//.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
3eb
3ec
3cd
len'n: (n' <= n)%N
lemm': (m <= m')%N
PP'i: forall i : nat, (n <= i < m)%N -> P i -> P' i
{subset [seq i <- index_iota n m | P i]
     <= [seq i <- index_iota n' m' | P' i]}
move=> i; rewrite !mem_filter !mem_index_iota => /and3P[Pi ni im].
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
3eb
3ec
3cd
3f3
3f4
3f5
i: nat_eqType
Pi: P i
ni: (n <= i)%N
im: (i < m)%N
[&& P' i, (n' <= i)%N & (i < m')%N]
by rewrite PP'i ?ni//= (leq_trans _ ni)// (leq_trans im).
Qed.

Lemma le_big_nat n m n' m' [P] [F : nat -> R] : (n' <= n)%N -> (m <= m')%N ->
  le (\big[op/x]_(n <= i < m | P i) F i) (\big[op/x]_(n' <= i < m' | P i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
3eb
P: nat -> bool
3cd
(n' <= n)%N ->
(m <= m')%N ->
le (\big[op/x]_(n <= i < m | P i) F i)
  (\big[op/x]_(n' <= i < m' | P i) F i)
Proof.
401 by move=> len'n lemm'; rewrite le_big_nat_cond. Qed.

Lemma le_big_ord_cond n m (P P' : {pred nat}) (F : nat -> R) :
    (n <= m)%N -> (forall i : 'I_n, P i -> P' i) ->
  le (\big[op/x]_(i < n | P i) F i) (\big[op/x]_(i < m | P' i) F i).
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
3cb
3ec
3cd
(n <= m)%N ->
(forall i : 'I_n, P i -> P' i) ->
le (\big[op/x]_(i < n | P i) F i)
  (\big[op/x]_(i < m | P' i) F i)
Proof.
408
move=> nm PP'; rewrite -!big_mkord le_big_nat_cond//= => i ni.
2d7
2d8
2d9
2da
2e1
2e8
2e9
219
35c
35d
35e
3cb
3ec
3cd
nm: (n <= m)%N
PP': forall i : 'I_n, P i -> P' i
i: nat
ni: (i < n)%N
P i -> P' i
by have := PP' (Ordinal ni).
Qed.

End SemiGroupProperties.

Section bigmaxmin.
Local Notation max := Order.max.
Local Notation min := Order.min.
Local Open Scope order_scope.
Variables (d : _) (T : porderType d).
Variables (I : Type) (r : seq I) (f : I -> T) (x0 x : T) (P : pred I).

Lemma bigmax_le :
  x0 <= x -> (forall i, P i -> f i <= x) -> \big[max/x0]_(i <- r | P i) f i <= x.
5f
60
15c
15d
f: I -> T
x0, x: T
15e
x0 <= x ->
(forall i : I, P i -> f i <= x) ->
\big[max/x0]_(i <- r | P i) f i <= x
Proof.
417 by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed.

Lemma bigmax_lt :
  x0 < x -> (forall i, P i -> f i < x) -> \big[max/x0]_(i <- r | P i) f i < x.
419
x0 < x ->
(forall i : I, P i -> f i < x) ->
\big[max/x0]_(i <- r | P i) f i < x
Proof.
41f by move=> ? ?; elim/big_ind: _ => // *; rewrite maxElt; case: ifPn. Qed.

Lemma lt_bigmin :
  x < x0 -> (forall i, P i -> x < f i) -> x < \big[min/x0]_(i <- r | P i) f i.
419
x < x0 ->
(forall i : I, P i -> x < f i) ->
x < \big[min/x0]_(i <- r | P i) f i
Proof.
424 by move=> ? ?; elim/big_ind: _ => // *; rewrite minElt; case: ifPn. Qed.

Lemma le_bigmin :
  x <= x0 -> (forall i, P i -> x <= f i) -> x <= \big[min/x0]_(i <- r | P i) f i.
419
x <= x0 ->
(forall i : I, P i -> x <= f i) ->
x <= \big[min/x0]_(i <- r | P i) f i
Proof.
429 by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed.

End bigmaxmin.

Section bigmax.
Local Notation max := Order.max.
Local Open Scope order_scope.
Variables (d : unit) (T : orderType d).

Section bigmax_Type.
Variables (I : Type) (r : seq I) (x : T).
Implicit Types (P a : pred I) (F : I -> T).

Lemma bigmax_mkcond P F : \big[max/x]_(i <- r | P i) F i =
  \big[max/x]_(i <- r) (if P i then F i else x).
5f
13d
15c
15d
f4
15e
F: I -> T
\big[max/x]_(i <- r | P i) F i =
\big[max/x]_(i <- r) (if P i then F i else x)
Proof.
42e by rewrite big_mkcond_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed.

Lemma bigmax_split P F1 F2 :
  \big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) =
  max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i).
5f
13d
15c
15d
f4
15e
F1, F2: I -> T
\big[max/x]_(i <- r | P i) max (F1 i) (F2 i) =
max (\big[max/x]_(i <- r | P i) F1 i)
  (\big[max/x]_(i <- r | P i) F2 i)
Proof.
435 by rewrite big_split_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed.

Lemma bigmax_idl P F :
  \big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i).
430
\big[max/x]_(i <- r | P i) F i =
max x (\big[max/x]_(i <- r | P i) F i)
Proof.
43c by rewrite maxC big_id_idem ?maxxx//; exact: maxA. Qed.

Lemma bigmax_idr P F :
  \big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x.
430
\big[max/x]_(i <- r | P i) F i =
max (\big[max/x]_(i <- r | P i) F i) x
Proof.
441 by rewrite [LHS]bigmax_idl maxC. Qed.

Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i =
  max (\big[max/x]_(i <- r | P i && a i) F i)
      (\big[max/x]_(i <- r | P i && ~~ a i) F i).
5f
13d
15c
15d
f4
342
431
\big[max/x]_(i <- r | P i) F i =
max (\big[max/x]_(i <- r | P i && a i) F i)
  (\big[max/x]_(i <- r | P i && ~~ a i) F i)
Proof.
446 by rewrite (bigID_idem maxA maxC _ _ a) ?maxxx. Qed.

End bigmax_Type.

Let le_maxr_id (x y : T) : x <= max x y.
5f
13d
61
x <= max x y Proof.
44c by rewrite le_maxr lexx. Qed.

Lemma sub_bigmax [x0] I s (P P' : {pred I}) (F : I -> T) :
     (forall i, P i -> P' i) ->
  \big[max/x0]_(i <- s | P i) F i <= \big[max/x0]_(i <- s | P' i) F i.
5f
13d
le_maxr_id: forall x y : T, x <= max x y
x0: T
15c
35f
360
431
(forall i : I, P i -> P' i) ->
\big[max/x0]_(i <- s | P i) F i <=
\big[max/x0]_(i <- s | P' i) F i
Proof.
452 exact: (sub_big maxA maxC). Qed.

Lemma sub_bigmax_seq [x0] (I : eqType) s s' P (F : I -> T) : {subset s <= s'} ->
  \big[max/x0]_(i <- s | P i) F i <= \big[max/x0]_(i <- s' | P i) F i.
5f
13d
455
456
1eb
3a6
305
431
{subset s <= s'} ->
\big[max/x0]_(i <- s | P i) F i <=
\big[max/x0]_(i <- s' | P i) F i
Proof.
45a exact: (sub_big_idem maxA maxC maxxx). Qed.

Lemma sub_bigmax_cond [x0] (I : eqType) s s' P P' (F : I -> T) :
    {subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
  \big[max/x0]_(i <- s | P i) F i <= \big[max/x0]_(i <- s' | P' i) F i.
5f
13d
455
456
1eb
37f
3b2
431
{subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
\big[max/x0]_(i <- s | P i) F i <=
\big[max/x0]_(i <- s' | P' i) F i
Proof.
460 exact: (sub_big_idem_cond maxA maxC maxxx). Qed.

Lemma sub_in_bigmax [x0] [I : eqType] (s : seq I) (P P' : {pred I}) (F : I -> T) :
    {in s, forall i, P i -> P' i} ->
  \big[max/x0]_(i <- s | P i) F i <= \big[max/x0]_(i <- s | P' i) F i.
5f
13d
455
456
1eb
35f
360
431
{in s, forall i : I, P i -> P' i} ->
\big[max/x0]_(i <- s | P i) F i <=
\big[max/x0]_(i <- s | P' i) F i
Proof.
466 exact: (sub_in_big maxA maxC). Qed.

Lemma le_bigmax_nat [x0] n m n' m' P (F : nat -> T) : n' <= n -> m <= m' ->
  \big[max/x0]_(n <= i < m | P i) F i <= \big[max/x0]_(n' <= i < m' | P i) F i.
5f
13d
455
456
n, m, n', m': Order.NatOrder.porderType
404
F: nat -> T
n' <= n ->
m <= m' ->
\big[max/x0]_(n <= i < m | P i) F i <=
\big[max/x0]_(n' <= i < m' | P i) F i
Proof.
46c exact: (le_big_nat maxA maxC). Qed.

Lemma le_bigmax_nat_cond [x0] n m n' m' (P P' : {pred nat}) (F : nat -> T) :
    (n' <= n)%N -> (m <= m')%N -> (forall i, n <= i < m -> P i -> P' i) ->
  \big[max/x0]_(n <= i < m | P i) F i <= \big[max/x0]_(n' <= i < m' | P' i) F i.
5f
13d
455
456
3eb
3ec
470
(n' <= n)%N ->
(m <= m')%N ->
(forall i : Order.NatOrder.porderType,
 n <= i < m -> P i -> P' i) ->
\big[max/x0]_(n <= i < m | P i) F i <=
\big[max/x0]_(n' <= i < m' | P' i) F i
Proof.
474 exact: (le_big_nat_cond maxA maxC). Qed.

Lemma le_bigmax_ord [x0] n m (P : {pred nat}) (F : nat -> T) : (n <= m)%N ->
  \big[max/x0]_(i < n | P i) F i <= \big[max/x0]_(i < m | P i) F i.
5f
13d
455
456
3cb
3cc
470
(n <= m)%N ->
\big[max/x0]_(i < n | P i) F i <=
\big[max/x0]_(i < m | P i) F i
Proof.
47a exact: (le_big_ord maxA maxC). Qed.

Lemma le_bigmax_ord_cond [x0] n m (P P' : {pred nat}) (F : nat -> T) :
    (n <= m)%N -> (forall i : 'I_n, P i -> P' i) ->
  \big[max/x0]_(i < n | P i) F i <= \big[max/x0]_(i < m | P' i) F i.
5f
13d
455
456
3cb
3ec
470
(n <= m)%N ->
(forall i : 'I_n, P i -> P' i) ->
\big[max/x0]_(i < n | P i) F i <=
\big[max/x0]_(i < m | P' i) F i
Proof.
480 exact: (le_big_ord_cond maxA maxC). Qed.

Lemma subset_bigmax [x0] [I : finType] (A A' P : {pred I}) (F : I -> T) :
    A \subset A' ->
  \big[max/x0]_(i in A | P i) F i <= \big[max/x0]_(i in A' | P i) F i.
5f
13d
455
456
354
3d4
431
A \subset A' ->
\big[max/x0]_(i in A | P i) F i <=
\big[max/x0]_(i in A' | P i) F i
Proof.
486 exact: (subset_big maxA maxC). Qed.

Lemma subset_bigmax_cond [x0] (I : finType) (A A' P P' : {pred I}) (F : I -> T) :
    [set i in A | P i]  \subset [set i in A' | P' i] ->
  \big[max/x0]_(i in A | P i) F i <= \big[max/x0]_(i in A' | P' i) F i.
5f
13d
455
456
354
3e4
431
[set i in A | P i] \subset [set i in A' | P' i] ->
\big[max/x0]_(i in A | P i) F i <=
\big[max/x0]_(i in A' | P' i) F i
Proof.
48c exact: (subset_big_cond maxA maxC). Qed.

Section bigmax_finType.
Variables (I : finType) (x : T).
Implicit Types (P : pred I) (F : I -> T).

Lemma bigmaxD1 j P F : P j ->
  \big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i).
5f
13d
455
354
f4
355
15e
431
P j ->
\big[max/x]_(i | P i) F i =
max (F j) (\big[max/x]_(i | P i && (i != j)) F i)
Proof.
492 by move/(bigD1_AC maxA maxC) ->. Qed.

Lemma le_bigmax_cond j P F : P j -> F j <= \big[max/x]_(i | P i) F i.
494
P j -> F j <= \big[max/x]_(i | P i) F i
Proof.
498 by move=> Pj; rewrite (bigmaxD1 _ Pj) le_maxr lexx. Qed.

Lemma le_bigmax F j : F j <= \big[max/x]_i F i.
5f
13d
455
354
f4
431
355
F j <= \big[max/x]_i F i
Proof.
49d exact: le_bigmax_cond. Qed.

(* NB: as of [2022-08-02], bigop.bigmax_sup already exists for nat *)
Lemma bigmax_sup j P m F : P j -> m <= F j -> m <= \big[max/x]_(i | P i) F i.
5f
13d
455
354
f4
355
15e
m: T
431
P j -> m <= F j -> m <= \big[max/x]_(i | P i) F i
Proof.
4a3 by move=> Pj ?; apply: le_trans (le_bigmax_cond _ Pj). Qed.

Lemma bigmax_leP m P F : reflect (x <= m /\ forall i, P i -> F i <= m)
                                 (\big[max/x]_(i | P i) F i <= m).
5f
13d
455
354
x, m: T
15e
431
reflect (x <= m /\ (forall i : I, P i -> F i <= m))
  (\big[max/x]_(i | P i) F i <= m)
Proof.
4aa
apply: (iffP idP) => [|[? ?]]; last exact: bigmax_le.
4ac
\big[max/x]_(i | P i) F i <= m ->
x <= m /\ (forall i : I, P i -> F i <= m)
rewrite bigmax_idl le_maxl => /andP[-> leFm]; split=> // i Pi.
5f
13d
455
354
4ad
15e
431
leFm: \big[max/x]_(i | P i) F i <= m
1e4
3fc
F i <= m
by apply: le_trans leFm; exact: le_bigmax_cond.
Qed.

Lemma bigmax_ltP m P F :
  reflect (x < m /\ forall i, P i -> F i < m) (\big[max/x]_(i | P i) F i < m).
4ac
reflect (x < m /\ (forall i : I, P i -> F i < m))
  (\big[max/x]_(i | P i) F i < m)
Proof.
4bb
apply: (iffP idP) => [|[? ?]]; last exact: bigmax_lt.
4ac
\big[max/x]_(i | P i) F i < m ->
x < m /\ (forall i : I, P i -> F i < m)
rewrite bigmax_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi.
5f
13d
455
354
4ad
15e
431
ltFm: \big[max/x]_(i | P i) F i < m
1e4
3fc
F i < m
by apply: le_lt_trans ltFm; exact: le_bigmax_cond.
Qed.

Lemma bigmax_eq_arg j P F : P j -> (forall i, P i -> x <= F i) ->
  \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i].
494
P j ->
(forall i : I, P i -> x <= F i) ->
\big[max/x]_(i | P i) F i =
F [arg max_(i > j | P i) F i]
Proof.
4ca
move=> Pi0; case: arg_maxP => //= i Pi PF PxF.
5f
13d
455
354
f4
355
15e
431
Pi0: P j
1e4
3fc
PF: forall j : I, P j -> F j <= F i
PxF: forall i : I, P i -> x <= F i
\big[max/x]_(i | P i) F i = F i
apply/eqP; rewrite eq_le le_bigmax_cond // andbT.
4d1
\big[max/x]_(i | P i) F i <= F i
by apply/bigmax_leP; split => //; exact: PxF.
Qed.

Lemma eq_bigmax j P F : P j -> (forall i, P i -> x <= F i) ->
  {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}.
494
P j ->
(forall i : I, P i -> x <= F i) ->
{i0 : I | i0 \in I & \big[max/x]_(i | P i) F i = F i0}
Proof.
4db by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists. Qed.

Lemma le_bigmax2 P F1 F2 : (forall i, P i -> F1 i <= F2 i) ->
  \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i.
5f
13d
455
354
f4
15e
438
(forall i : I, P i -> F1 i <= F2 i) ->
\big[max/x]_(i | P i) F1 i <=
\big[max/x]_(i | P i) F2 i
Proof.
4e0
move=> FG; elim/big_ind2 : _ => // a b e f ba fe.
5f
13d
455
354
f4
15e
438
FG: forall i : I, P i -> F1 i <= F2 i
a, b, e, f: T
ba: b <= a
fe: f <= e
max b f <= max a e
rewrite le_maxr 2!le_maxl ba fe /= andbT; have [//|/= af] := leP f a.
5f
13d
455
354
f4
15e
438
4e9
4ea
4eb
4ec
af: a < f
b <= e
by rewrite (le_trans ba) // (le_trans _ fe) // ltW.
Qed.

End bigmax_finType.

End bigmax.
Arguments bigmax_mkcond {d T I r}.
Arguments bigmaxID {d T I r}.
Arguments bigmaxD1 {d T I x} j.
Arguments bigmax_sup {d T I x} j.
Arguments bigmax_eq_arg {d T I} x j.
Arguments eq_bigmax {d T I x} j.

Section bigmin.
Local Notation min := Order.min.
Local Open Scope order_scope.
Variables (d : _) (T : orderType d).

Section bigmin_Type.
Variable (I : Type) (r : seq I) (x : T).
Implicit Types (P a : pred I) (F : I -> T).

Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i =
   \big[min/x]_(i <- r) (if P i then F i else x).
430
\big[min/x]_(i <- r | P i) F i =
\big[min/x]_(i <- r) (if P i then F i else x)
Proof.
4f5 rewrite big_mkcond_idem ?minxx//; [exact: minA|exact: minC]. Qed.

Lemma bigmin_split P F1 F2 :
  \big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) =
  min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i).
437
\big[min/x]_(i <- r | P i) min (F1 i) (F2 i) =
min (\big[min/x]_(i <- r | P i) F1 i)
  (\big[min/x]_(i <- r | P i) F2 i)
Proof.
4fa rewrite big_split_idem ?minxx//; [exact: minA|exact: minC]. Qed.

Lemma bigmin_idl P F :
  \big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i).
430
\big[min/x]_(i <- r | P i) F i =
min x (\big[min/x]_(i <- r | P i) F i)
Proof.
4ff rewrite minC big_id_idem ?minxx//; exact: minA. Qed.

Lemma bigmin_idr P F :
  \big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x.
430
\big[min/x]_(i <- r | P i) F i =
min (\big[min/x]_(i <- r | P i) F i) x
Proof.
504 by rewrite [LHS]bigmin_idl minC. Qed.

Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i =
  min (\big[min/x]_(i <- r | P i && a i) F i)
      (\big[min/x]_(i <- r | P i && ~~ a i) F i).
448
\big[min/x]_(i <- r | P i) F i =
min (\big[min/x]_(i <- r | P i && a i) F i)
  (\big[min/x]_(i <- r | P i && ~~ a i) F i)
Proof.
509 by rewrite (bigID_idem minA minC _ _ a) ?minxx. Qed.

End bigmin_Type.

Let le_minr_id (x y : T) : x >= min x y.
44e
min x y <= x Proof.
50e by rewrite le_minl lexx. Qed.

Lemma sub_bigmin [x0] I s (P P' : {pred I}) (F : I -> T) :
     (forall i, P' i -> P i) ->
  \big[min/x0]_(i <- s | P i) F i <= \big[min/x0]_(i <- s | P' i) F i.
5f
13d
le_minr_id: forall x y : T, min x y <= x
456
15c
35f
360
431
(forall i : I, P' i -> P i) ->
\big[min/x0]_(i <- s | P i) F i <=
\big[min/x0]_(i <- s | P' i) F i
Proof.
513 exact: (sub_big minA minC ge_refl). Qed.

Lemma sub_bigmin_cond [x0] (I : eqType) s s' P P' (F : I -> T) :
    {subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
  \big[min/x0]_(i <- s' | P' i) F i <= \big[min/x0]_(i <- s | P i) F i.
5f
13d
516
456
1eb
37f
3b2
431
{subset [seq i <- s | P i] <= [seq i <- s' | P' i]} ->
\big[min/x0]_(i <- s' | P' i) F i <=
\big[min/x0]_(i <- s | P i) F i
Proof.
51a exact: (sub_big_idem_cond minA minC minxx ge_refl). Qed.

Lemma sub_bigmin_seq [x0] (I : eqType) s s' P (F : I -> T) : {subset s' <= s} ->
  \big[min/x0]_(i <- s | P i) F i <= \big[min/x0]_(i <- s' | P i) F i.
5f
13d
516
456
1eb
3a6
305
431
{subset s' <= s} ->
\big[min/x0]_(i <- s | P i) F i <=
\big[min/x0]_(i <- s' | P i) F i
Proof.
520 exact: (sub_big_idem minA minC minxx ge_refl). Qed.

Lemma sub_in_bigmin [x0] [I : eqType] (s : seq I) (P P' : {pred I}) (F : I -> T) :
    {in s, forall i, P' i -> P i} ->
  \big[min/x0]_(i <- s | P i) F i <= \big[min/x0]_(i <- s | P' i) F i.
5f
13d
516
456
1eb
35f
360
431
{in s, forall i : I, P' i -> P i} ->
\big[min/x0]_(i <- s | P i) F i <=
\big[min/x0]_(i <- s | P' i) F i
Proof.
526 exact: (sub_in_big minA minC ge_refl). Qed.

Lemma le_bigmin_nat [x0] n m n' m' P (F : nat -> T) :
  (n <= n')%N -> (m' <= m)%N ->
  \big[min/x0]_(n <= i < m | P i) F i <= \big[min/x0]_(n' <= i < m' | P i) F i.
5f
13d
516
456
3eb
404
470
(n <= n')%N ->
(m' <= m)%N ->
\big[min/x0]_(n <= i < m | P i) F i <=
\big[min/x0]_(n' <= i < m' | P i) F i
Proof.
52c exact: (le_big_nat minA minC ge_refl). Qed.

Lemma le_bigmin_nat_cond [x0] n m n' m' (P P' : pred nat) (F : nat -> T) :
    (n <= n')%N -> (m' <= m)%N -> (forall i, n' <= i < m' -> P' i -> P i) ->
  \big[min/x0]_(n <= i < m | P i) F i <= \big[min/x0]_(n' <= i < m' | P' i) F i.
5f
13d
516
456
3eb
P, P': pred nat
470
(n <= n')%N ->
(m' <= m)%N ->
(forall i : Order.NatOrder.porderType,
 n' <= i < m' -> P' i -> P i) ->
\big[min/x0]_(n <= i < m | P i) F i <=
\big[min/x0]_(n' <= i < m' | P' i) F i
Proof.
532 exact: (le_big_nat_cond minA minC ge_refl). Qed.

Lemma le_bigmin_ord [x0] n m (P : pred nat) (F : nat -> T) : (m <= n)%N ->
  \big[min/x0]_(i < n | P i) F i <= \big[min/x0]_(i < m | P i) F i.
5f
13d
516
456
3cb
P: pred nat
470
(m <= n)%N ->
\big[min/x0]_(i < n | P i) F i <=
\big[min/x0]_(i < m | P i) F i
Proof.
539 exact: (le_big_ord minA minC ge_refl). Qed.

Lemma le_bigmin_ord_cond [x0] n m (P P' : pred nat) (F : nat -> T) :
    (m <= n)%N -> (forall i : 'I_m, P' i -> P i) ->
  \big[min/x0]_(i < n | P i) F i <= \big[min/x0]_(i < m | P' i) F i.
5f
13d
516
456
3cb
535
470
(m <= n)%N ->
(forall i : 'I_m, P' i -> P i) ->
\big[min/x0]_(i < n | P i) F i <=
\big[min/x0]_(i < m | P' i) F i
Proof.
540 exact: (le_big_ord_cond minA minC ge_refl). Qed.

Lemma subset_bigmin [x0] [I : finType] [A A' P : {pred I}] (F : I -> T) :
    A' \subset A ->
  \big[min/x0]_(i in A | P i) F i <= \big[min/x0]_(i in A' | P i) F i.
5f
13d
516
456
354
3d4
431
A' \subset A ->
\big[min/x0]_(i in A | P i) F i <=
\big[min/x0]_(i in A' | P i) F i
Proof.
546 exact: (subset_big minA minC ge_refl). Qed.

Lemma subset_bigmin_cond [x0] (I : finType) (A A' P P' : {pred I}) (F : I -> T) :
    [set i in A' | P' i]  \subset [set i in A | P i] ->
  \big[min/x0]_(i in A | P i) F i <= \big[min/x0]_(i in A' | P' i) F i.
5f
13d
516
456
354
3e4
431
[set i in A' | P' i] \subset [set i in A | P i] ->
\big[min/x0]_(i in A | P i) F i <=
\big[min/x0]_(i in A' | P' i) F i
Proof.
54c exact: (subset_big_cond minA minC ge_refl). Qed.

Section bigmin_finType.
Variable (I : finType) (x : T).
Implicit Types (P : pred I) (F : I -> T).

Lemma bigminD1 j P F : P j ->
  \big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i).
5f
13d
516
354
f4
355
15e
431
P j ->
\big[min/x]_(i | P i) F i =
min (F j) (\big[min/x]_(i | P i && (i != j)) F i)
Proof.
552 by move/(bigD1_AC minA minC) ->. Qed.

Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j.
554
P j -> \big[min/x]_(i | P i) F i <= F j
Proof.
558
have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih.
5f
13d
516
354
f4
355
15e
431
1e4
l: seq I
ih: j \in l ->
P j ->
reducebig x l
  (fun i : I => BigBody i min (P i) (F i)) <= 
F j
j \in i :: l ->
P j ->
(if P i
 then
  min (F i)
    (reducebig x l
       (fun i : I => BigBody i min (P i) (F i)))
 else
  reducebig x l
    (fun i : I => BigBody i min (P i) (F i))) <= F j
rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite le_minl lexx.
5f
13d
516
354
f4
355
15e
431
1e4
560
561
leminlfi: P j ->
reducebig x l
  (fun i : I => BigBody i min (P i) (F i)) <=
F j
Pi: P j
(if P i
 then
  min (F i)
    (reducebig x l
       (fun i : I => BigBody i min (P i) (F i)))
 else
  reducebig x l
    (fun i : I => BigBody i min (P i) (F i))) <= F j
by case: ifPn => Pj; [rewrite le_minl leminlfi// orbC|exact: leminlfi].
Qed.

Lemma bigmin_le j F : \big[min/x]_i F i <= F j.
5f
13d
516
354
f4
355
431
\big[min/x]_i F i <= F j
Proof.
56b exact: bigmin_le_cond. Qed.

Lemma bigmin_inf j P m F : P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m.
5f
13d
516
354
f4
355
15e
4a6
431
P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m
Proof.
571 by move=> Pj ?; apply: le_trans (bigmin_le_cond _ Pj) _. Qed.

Lemma bigmin_geP m P F : reflect (m <= x /\ forall i, P i -> m <= F i)
                                 (m <= \big[min/x]_(i | P i) F i).
5f
13d
516
354
4ad
15e
431
reflect (m <= x /\ (forall i : I, P i -> m <= F i))
  (m <= \big[min/x]_(i | P i) F i)
Proof.
577
apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: le_bigmin].
5f
13d
516
354
4ad
15e
431
lemFi: m <= \big[min/x]_(i | P i) F i
m <= x
57f
forall i : I, P i -> m <= F i
-
57d by rewrite (le_trans lemFi)// bigmin_idl le_minl lexx.
57f
584
-
587 by move=> i Pi; rewrite (le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx.
Qed.

Lemma bigmin_gtP m P F :
  reflect (m < x /\ forall i, P i -> m < F i) (m < \big[min/x]_(i | P i) F i).
579
reflect (m < x /\ (forall i : I, P i -> m < F i))
  (m < \big[min/x]_(i | P i) F i)
Proof.
58b
apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: lt_bigmin].
5f
13d
516
354
4ad
15e
431
lemFi: m < \big[min/x]_(i | P i) F i
m < x
592
forall i : I, P i -> m < F i
-
590 by rewrite (lt_le_trans lemFi)// bigmin_idl le_minl lexx.
592
597
-
59a by move=> i Pi; rewrite (lt_le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx.
Qed.

Lemma bigmin_eq_arg j P F : P j -> (forall i, P i -> F i <= x) ->
  \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i].
554
P j ->
(forall i : I, P i -> F i <= x) ->
\big[min/x]_(i | P i) F i =
F [arg min_(i < j | P i) F i]
Proof.
59e
move=> Pi0; case: arg_minP => //= i Pi PF PFx.
5f
13d
516
354
f4
355
15e
431
4d2
1e4
3fc
PF: forall j : I, P j -> F i <= F j
PFx: forall i : I, P i -> F i <= x
\big[min/x]_(i | P i) F i = F i
apply/eqP; rewrite eq_le bigmin_le_cond //=.
5a5
F i <= \big[min/x]_(i | P i) F i
by apply/bigmin_geP; split => //; exact: PFx.
Qed.

Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) ->
  {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}.
554
P j ->
(forall i : I, P i -> F i <= x) ->
{i0 : I | i0 \in I & \big[min/x]_(i | P i) F i = F i0}
Proof.
5ae by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists. Qed.

End bigmin_finType.

End bigmin.
Arguments bigmin_mkcond {d T I r}.
Arguments bigminID {d T I r}.
Arguments bigminD1 {d T I x} j.
Arguments bigmin_inf {d T I x} j.
Arguments bigmin_eq_arg {d T I} x j.
Arguments eq_bigmin {d T I x} j.

Section onem.
Variable R : numDomainType.
Implicit Types r : R.

Definition onem r := 1 - r.
Local Notation "`1- r" := (onem r).

Lemma onem0 : `1-0 = 1.
15b
`1-0 = 1 Proof.
5b3 by rewrite /onem subr0. Qed.

Lemma onem1 : `1-1 = 0.
5b5
`1-1 = 0 Proof.
5b9 by rewrite /onem subrr. Qed.

Lemma onemK r : `1-(`1-r) = r.
1c8
`1-(`1-r) = r
Proof.
5be by rewrite /onem opprB addrCA subrr addr0. Qed.

Lemma add_onemK r : r + `1- r = 1.
1c8
r + `1-r = 1
Proof.
5c3 by rewrite /onem addrC subrK. Qed.

Lemma onem_gt0 r : r < 1 -> 0 < `1-r.
1c8
r < 1 -> 0 < `1-r Proof.
5c8 by rewrite subr_gt0. Qed.

Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r.
1c8
r <= 1 -> 0 <= `1-r
Proof.
5cd by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed.

Lemma onem_le1 r : 0 <= r -> `1-r <= 1.
1c8
0 <= r -> `1-r <= 1
Proof.
5d2 by rewrite ler_subl_addr ler_addl. Qed.

Lemma onem_lt1 r : 0 < r -> `1-r < 1.
1c8
0 < r -> `1-r < 1
Proof.
5d7 by rewrite ltr_subl_addr ltr_addl. Qed.

Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n).
15b
1c9
16b
0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n)
Proof.
5dc by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed.

Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1.
5de
0 < r -> `1-(r ^+ n) < 1
Proof.
5e2 by move=> ?; rewrite onem_lt1// exprn_gt0. Qed.

Lemma onemD r s : `1-(r + s) = `1-r - s.
15b
r, s: R
`1-(r + s) = `1-r - s
Proof.
5e7 by rewrite /onem addrAC opprD addrA addrAC. Qed.

Lemma onemMr r s : s * `1-r = s - s * r.
5e9
s * `1-r = s - s * r
Proof.
5ee by rewrite /onem mulrBr mulr1. Qed.

Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s.
5e9
`1-(r * s) = `1-r + `1-s - `1-r * `1-s
Proof.
5f3
rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA.
5e9
1 - r * s = 1 - r + (1 - s + (s - r * s - (1 - r)))
by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK.
Qed.

End onem.
Notation "`1- r" := (onem r) : ring_scope.

Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.
a, b: int
0 <= a -> a <= b -> (`|a| <= `|b|)%N
Proof.
5fc by case: a => //= n _; case: b. Qed.

Lemma ler_gtP (R : numFieldType) (x y : R) :
  reflect (forall z, z > y -> x <= z) (x <= y).
21f
reflect (forall z : R, y < z -> x <= z) (x <= y)
Proof.
603
apply: (equivP (ler_addgt0Pr _ _)); split=> [xy z|xz e e_gt0].
10d
206
xy: forall e : R, 0 < e -> x <= y + e
z: R
y < z -> x <= z
10d
206
xz: forall z : R, y < z -> x <= z
251
252
x <= y + e
  by rewrite -subr_gt0 => /xy; rewrite addrC addrNK.
610
612
by apply: xz; rewrite -[ltLHS]addr0 ler_lt_add.
Qed.

Lemma ler_ltP (R : numFieldType) (x y : R) :
  reflect (forall z, z < x -> z <= y) (x <= y).
21f
reflect (forall z : R, z < x -> z <= y) (x <= y)
Proof.
617
apply: (equivP (ler_addgt0Pr _ _)); split=> [xy z|xz e e_gt0].
60a
z < x -> z <= y
10d
206
xz: forall z : R, z < x -> z <= y
251
252
612
  by rewrite -subr_gt0 => /xy; rewrite addrCA -[leLHS]addr0 ler_add2l subr_ge0.
621
612
by rewrite -ler_subl_addr xz// -[ltRHS]subr0 ler_lt_sub.
Qed.

Definition inv_fun T (R : unitRingType) (f : T -> R) x := (f x)^-1%R.
Notation "f \^-1" := (inv_fun f) : ring_scope.
Arguments inv_fun {T R} _ _ /.

Definition bound_side d (T : porderType d) (c : bool) (x : itv_bound T) :=
  if x is BSide c' _ then c == c' else false.

Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : R) :
  x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e).
15b
x, y, e: R
x - y \is Num.real ->
(`|x - y| < e) = (x - e < y < x + e)
Proof.
627 by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed.

Definition proj {I} {T : I -> Type} i (f : forall i, T i) := f i.

Section DFunWith.
Variables (I : eqType) (T : I -> Type) (f : forall i, T i).

Definition dfwith i (x : T i) (j : I) : T j :=
  if (i =P j) is ReflectT ij then ecast j (T j) ij x else f j.

Lemma dfwithin i x : dfwith x i = x.
1eb
T: I -> Type
f: forall i : I, T i
1e4
x: T i
dfwith x i = x
Proof.
62e by rewrite /dfwith; case: eqP => // ii; rewrite eq_axiomK. Qed.

Lemma dfwithout i (x : T i) j : i != j -> dfwith x j = f j.
1eb
631
632
1e4
633
355
i != j -> dfwith x j = f j
Proof.
637 by rewrite /dfwith; case: eqP. Qed.

Variant dfwith_spec i (x : T i) : forall j, T j -> Type :=
  | DFunWithin : dfwith_spec x x
  | DFunWithout j : i != j -> dfwith_spec x (f j).

Lemma dfwithP i (x : T i) (j : I) : dfwith_spec x (dfwith x j).
639
dfwith_spec x (dfwith x j)
Proof.
63d
by case: (eqVneq i j) => [<-|nij];
   [rewrite dfwithin|rewrite dfwithout//]; constructor.
Qed.

Lemma projK i (x : T i) : cancel (@dfwith i) (proj i).
630
cancel (dfwith (i:=i)) (proj i)
Proof.
642 by move=> z; rewrite /proj dfwithin. Qed.

End DFunWith.
Arguments dfwith {I T} f i x.

Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).