Library mathcomp.classical.mathcomp_extra

(* 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.
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) f \min g := fun x => Num.min (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.

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).

Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I)
   (P Q : I → T → Prop) : T →
    (∀ x : I, D x → {y : T | P x y & Q x y }) →
  {f : ∀ x : I, T | ∀ x : I, D x → P x (f x) & ∀ x : I, D x → Q x (f x)}.

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.

Lemma olift_comp aT rT sT (f : aT → rT) (g : rT → sT) :
  olift (g \o f) = olift g \o f.

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.

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))}.

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 }.

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')}.

Lemma eqbRL (b1 b2 : bool) : b1 = b2 → b2 → b1.

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.
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.
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.

Lemma leBSide x y b b' :
  ((BSide b x ≤ BSide b' y ) = (x < y ?<= if b' ==> b ))%O.

Definition lteBSide := (ltBSide , leBSide ).

Let BLeft_ltE x y b : (BSide b x < BLeft y)%O = (x < y)%O.
Let BRight_leE x y b : (BSide b x ≤ BRight y)%O = (x ≤ y)%O.
Let BRight_BLeft_leE x y : (BRight x ≤ BLeft y)%O = (x < y)%O.
Let BLeft_BRight_ltE x y : (BLeft x < BRight y)%O = (x ≤ y)%O.
Let BRight_BSide_ltE x y b : (BRight x < BSide b y)%O = (x < y)%O.
Let BLeft_BSide_leE x y b : (BLeft x ≤ BSide b y)%O = (x ≤ y)%O.
Let BSide_ltE x y b : (BSide b x < BSide b y)%O = (x < y)%O.
Let BSide_leE x y b : (BSide b x ≤ BSide b y)%O = (x ≤ y)%O.
Let BInfty_leE a : (a ≤ BInfty T false)%O.
Let BInfty_geE a : (BInfty T true ≤ a)%O.
Let BInfty_le_eqE a : (BInfty T false ≤ a)%O = (a == BInfty T false ).
Let BInfty_ge_eqE a : (a ≤ BInfty T true)%O = (a == BInfty T true ).
Let BInfty_ltE a : (a < BInfty T false)%O = (a != BInfty T false ).
Let BInfty_gtE a : (BInfty T true < a)%O = (a != BInfty T true ).
Let BInfty_ltF a : (BInfty T false < a)%O = false.
Let BInfty_gtF a : (a < BInfty T true)%O = false.
Let BInfty_BInfty_ltE : (BInfty T true < BInfty T false)%O.

Lemma ltBRight_leBLeft (a : itv_bound T) (r : T) :
  (a < BRight r)%O = (a ≤ BLeft r)%O.
Lemma leBRight_ltBLeft (a : itv_bound T) (r : T) :
  (BRight r ≤ a)%O = (BLeft r < a)%O.

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)].

Lemma itv_split1U (a : itv_bound T) (x : T) : (BRight x ≤ a)%O →
  Interval (BLeft x) a =i [predU1 x & Interval (BRight x) a].

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.

Lemma miditv_le_left i b : (i .1 < i .2)%O → (BSide b (miditv i) ≤ i .2)%O.

Lemma miditv_ge_right i b : (i .1 < i .2)%O → (i .1 ≤ BSide b (miditv i))%O.

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.

Lemma predC_itvr a : [predC Interval a +oo%O] =i Interval -oo%O a.

Lemma predC_itv i : [predC i] =i [predU Interval -oo%O i .1 & Interval i .2 +oo%O].

End itv_porderType.

Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I → R) :
  (∀ i, P i → F i ≤ 0)%R → (\sum_(i <- r | P i) F i ≤ 0)%R.

Lemma enum_ord0 : enum 'I_0 = [::].

Lemma enum_ordSr n : enum 'I_n.+1 =
  rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max.

Lemma obindEapp {aT rT} (f : aT → option rT) : obind f = oapp f None.

Lemma omapEbind {aT rT} (f : aT → rT) : omap f = obind (olift f).

Lemma omapEapp {aT rT} (f : aT → rT) : omap f = oapp (olift f) None.

Lemma oappEmap {aT rT} (f : aT → rT) (y0 : rT) x :
  oapp f y0 x = odflt y0 (omap f x).

Lemma omap_comp aT rT sT (f : aT → rT) (g : rT → sT) :
  omap (g \o f) =1 omap g \o omap f.

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.

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')}.

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)}.

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')}.

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').

Lemma eqbLR (b1 b2 : bool) : b1 = b2 → b1 → b2.

Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R → (- r < r)%R.

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.

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.

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.

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.

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 ).

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.

Lemma ler_addgt0Pr x y : reflect (∀ e, e > 0 → x ≤ y + e) (x ≤ y).

Lemma ler_addgt0Pl x y : reflect (∀ e, e > 0 → x ≤ e + y) (x ≤ y).

Lemma in_segment_addgt0Pr x y z :
  reflect (∀ e, e > 0 → y \in `[x - e, z + e]) (y \in `[x, z]).

Lemma in_segment_addgt0Pl x y z :
  reflect (∀ e, e > 0 → y \in `[(- e + x), (e + z)]) (y \in `[x, z]).

Lemma lt_le a b : (∀ x, x < a → x < b ) → a ≤ b.

Lemma gt_ge a b : (∀ x, b < x → a < x ) → a ≤ b.

End lt_le_gt_ge.

Lemma itvxx d (T : porderType d) (x : T) : `[x, x] =i pred1 x.

Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).

Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ ≤ `[a, b]}.

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", left associativity).

Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R.

Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R.

To be backported to finmap

Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
    (f : X → nat) : A != fset0 →
  (∃ i , i \in A ∧ ∀ j, j \in A → f j ≤ f i)%nat.

Lemma image_nat_maximum n (f : nat → nat) :
  (∃ i , i ≤ n ∧ ∀ j, j ≤ n → f j ≤ f i)%N.

Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
  #|` A| = (\sum_(i <- A) 1)%N.

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

MathComp 1.16.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.
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.
Let opAC : right_commutative op.

Hypothesis opyy : idempotent op.

Lemma opACE x y : oop (Some x) (Some y) = some (op x y).

Lemma oopA_subdef : associative oop.

Lemma oopx1_subdef : left_id None oop.
Lemma oop1x_subdef : right_id None oop.

Lemma oopC_subdef : commutative oop.

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).

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)).

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.

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.

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.

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.

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).

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).

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.

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).

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.

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).

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

Lemma sub_big I [s] (P P' : {pred I }) (F : I → R) : (∀ i, P i → P' i ) →
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).

Lemma sub_big_seq (I : eqType) s s' P (F : I → R) :
  (∀ 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).

Lemma sub_big_seq_cond (I : eqType) s s' P P' (F : I → R) :
    (∀ 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).

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).

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).

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).

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).

Lemma sub_in_big [I : eqType] (s : seq I) (P P' : {pred I }) (F : I → R) :
    {in s , ∀ i, P i → P' i } →
  le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).

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).

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).

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).

Lemma le_big_nat_cond n m n' m' (P P' : {pred nat }) (F : nat → R) :
    (n' ≤ n)%N → (m ≤ m')%N → (∀ 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).

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).

Lemma le_big_ord_cond n m (P P' : {pred nat }) (F : nat → R) :
    (n ≤ m)%N → (∀ 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).

End SemiGroupProperties.

Section bigmaxmin.
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 → (∀ i, P i → f i ≤ x ) → \big[max/x0]_(i <- r | P i) f i ≤ x.

Lemma bigmax_lt :
  x0 < x → (∀ i, P i → f i < x ) → \big[max/x0]_(i <- r | P i) f i < x.

Lemma lt_bigmin :
  x < x0 → (∀ i, P i → x < f i ) → x < \big[min/x0]_(i <- r | P i) f i.

Lemma le_bigmin :
  x ≤ x0 → (∀ i, P i → x ≤ f i ) → x ≤ \big[min/x0]_(i <- r | P i) f i.

End bigmaxmin.

Section bigmax.
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).

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).

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).

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.

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).

End bigmax_Type.

Let le_maxr_id (x y : T) : x ≤ max x y.

Lemma sub_bigmax [x0] I s (P P' : {pred I }) (F : I → T) :
     (∀ i, P i → P' i ) →
  \big[max/x0]_(i <- s | P i) F i ≤ \big[max/x0]_(i <- s | P' i) F i.

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.

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.

Lemma sub_in_bigmax [x0] [I : eqType] (s : seq I) (P P' : {pred I }) (F : I → T) :
    {in s , ∀ i, P i → P' i } →
  \big[max/x0]_(i <- s | P i) F i ≤ \big[max/x0]_(i <- s | P' i) F i.

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.

Lemma le_bigmax_nat_cond [x0] n m n' m' (P P' : {pred nat }) (F : nat → T) :
    (n' ≤ n)%N → (m ≤ m')%N → (∀ 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.

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.

Lemma le_bigmax_ord_cond [x0] n m (P P' : {pred nat }) (F : nat → T) :
    (n ≤ m)%N → (∀ 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.

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.

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.

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).

Lemma le_bigmax_cond j P F : P j → F j ≤ \big[max/x]_(i | P i) F i.

Lemma le_bigmax F j : F j ≤ \big[max/x]_i F i.

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.

Lemma bigmax_leP m P F : reflect (x ≤ m ∧ ∀ i, P i → F i ≤ m)
                                 (\big[max/x]_(i | P i) F i ≤ m).

Lemma bigmax_ltP m P F :
  reflect (x < m ∧ ∀ i, P i → F i < m) (\big[max/x]_(i | P i) F i < m).

Lemma bigmax_eq_arg j P F : P j → (∀ i, P i → x ≤ F i ) →
  \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i].

Lemma eq_bigmax j P F : P j → (∀ i, P i → x ≤ F i ) →
  {i0 | i0 \in P & \big[max/x]_(i | P i) F i = F i0 }.

Lemma le_bigmax2 P F1 F2 : (∀ i, P i → F1 i ≤ F2 i ) →
  \big[max/x]_(i | P i) F1 i ≤ \big[max/x]_(i | P i) F2 i.

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 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).

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).

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).

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.

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).

End bigmin_Type.

Let le_minr_id (x y : T) : x ≥ min x y.

Lemma sub_bigmin [x0] I s (P P' : {pred I }) (F : I → T) :
     (∀ i, P' i → P i ) →
  \big[min/x0]_(i <- s | P i) F i ≤ \big[min/x0]_(i <- s | P' i) F i.

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.

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.

Lemma sub_in_bigmin [x0] [I : eqType] (s : seq I) (P P' : {pred I }) (F : I → T) :
    {in s , ∀ i, P' i → P i } →
  \big[min/x0]_(i <- s | P i) F i ≤ \big[min/x0]_(i <- s | P' i) F i.

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.

Lemma le_bigmin_nat_cond [x0] n m n' m' (P P' : pred nat) (F : nat → T) :
    (n ≤ n')%N → (m' ≤ m)%N → (∀ 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.

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.

Lemma le_bigmin_ord_cond [x0] n m (P P' : pred nat) (F : nat → T) :
    (m ≤ n)%N → (∀ 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.

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.

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.

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).

Lemma bigmin_le_cond j P F : P j → \big[min/x]_(i | P i) F i ≤ F j.

Lemma bigmin_le j F : \big[min/x]_i F i ≤ F j.

Lemma bigmin_inf j P m F : P j → F j ≤ m → \big[min/x]_(i | P i) F i ≤ m.

Lemma bigmin_geP m P F : reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
                                 (m ≤ \big[min/x]_(i | P i) F i).

Lemma bigmin_gtP m P F :
  reflect (m < x ∧ ∀ i, P i → m < F i) (m < \big[min/x]_(i | P i) F i).

Lemma bigmin_eq_arg j P F : P j → (∀ i, P i → F i ≤ x ) →
  \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i].

Lemma eq_bigmin j P F : P j → (∀ i, P i → F i ≤ x ) →
  {i0 | i0 \in P & \big[min/x]_(i | P i) F i = F i0 }.

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.

End of MathComp 1.16.0 additions MathComp > 1.16 additions

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

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} _ _ _ /.

End of mathComp > 1.16 additions

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

Definition onem r := 1 - r.

Lemma onem0 : `1-0 = 1.

Lemma onem1 : `1-1 = 0.

Lemma onemK r : `1-(`1-r ) = r.

Lemma add_onemK r : r + `1- r = 1.

Lemma onem_gt0 r : r < 1 → 0 < `1-r.

Lemma onem_ge0 r : r ≤ 1 → 0 ≤ `1-r.

Lemma onem_le1 r : 0 ≤ r → `1-r ≤ 1.

Lemma onem_lt1 r : 0 < r → `1-r < 1.

Lemma onemX_ge0 r n : 0 ≤ r → r ≤ 1 → 0 ≤ `1-(r ^+ n ).

Lemma onemX_lt1 r n : 0 < r → `1-(r ^+ n ) < 1.

Lemma onemD r s : `1-(r + s ) = `1-r - s.

Lemma onemMr r s : s × `1-r = s - s × r.

Lemma onemM r s : `1-(r × s ) = `1-r + `1-s - `1-r × `1-s.

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

Lemma lez_abs2 (a b : int) : 0 ≤ a → a ≤ b → (`|a| ≤ `|b|)%N.

Lemma ler_gtP (R : numFieldType) (x y : R) :
  reflect (∀ z, z > y → x ≤ z) (x ≤ y).

Lemma ler_ltP (R : numFieldType) (x y : R) :
  reflect (∀ z, z < x → z ≤ y) (x ≤ y).

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 ).

Definition proj {I} {T : I → Type} i (f : ∀ i, T i) := f i.

Section DFunWith.
Variables (I : eqType) (T : I → Type) (f : ∀ 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.

Lemma dfwithout i (x : T i) j : i != j → dfwith x j = f j.

Variant dfwith_spec i (x : T i) : ∀ 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).

Lemma projK i (x : T i) : cancel (@dfwith i) (proj i).

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

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

Lemma ler_sqrt {R : rcfType} (a b : R) :
  (0 ≤ b → (Num.sqrt a ≤ Num.sqrt b ) = (a ≤ b ))%R.

Section order_min.
Variables (d : unit) (T : orderType d).
Import Order.
Local Open Scope order_scope.

Lemma lt_min_lt (x y z : T) : (min x z < min y z)%O → (x < y)%O.

End order_min.

MathComp 2.1 additions

From mathcomp Require Import poly.

Definition coefE :=
  (coef0, coef1, coefC, coefX, coefXn,
   coefZ, coefMC, coefCM, coefXnM, coefMXn, coefXM, coefMX, coefMNn, coefMn,
   coefN, coefB, coefD,
   coef_cons, coef_Poly, coef_poly,
   coef_deriv, coef_nderivn, coef_derivn, coef_map, coef_sum,
   coef_comp_poly).

Module Export Pdeg2.

Module Export Field.

Section Pdeg2Field.
Variable F : fieldType.
Hypothesis nz2 : 2%:R != 0 :> F.

Variable p : {poly F}.
Hypothesis degp : size p = 3%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let pneq0 : p != 0.
Let aneq0 : a != 0.
Let a2neq0 : 2%:R × a != 0.
Let sqa2neq0 : (2%:R × a) ^+ 2 != 0.

Let aa4 : 4%:R × a × a = (2%:R × a)^+2.

Let splitr (x : F) : x = x / 2%:R + x / 2%:R.

Let pE : p = a *: 'X^2 + b *: 'X + c%:P.

Let delta := b ^+ 2 - 4%:R × a × c.

Lemma deg2_poly_canonical :
  p = a *: (('X + (b / (2%:R × a))%:P)^+2 - (delta / (4%:R × a ^+ 2))%:P).

Variable r : F.
Hypothesis r_sqrt_delta : r ^+ 2 = delta.

Let r1 := (- b - r) / (2%:R × a).
Let r2 := (- b + r) / (2%:R × a).

Lemma deg2_poly_factor : p = a *: ('X - r1%:P) × ('X - r2%:P).

End Pdeg2Field.
End Field.

Module Real.

Section Pdeg2Real.

Variable F : realFieldType.

Section Pdeg2RealConvex.

Variable p : {poly F}.
Hypothesis degp : size p = 3%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Hypothesis age0 : 0 ≤ a.

Let delta := b ^+ 2 - 4%:R × a × c.

Let pneq0 : p != 0.
Let aneq0 : a != 0.
Let agt0 : 0 < a.
Let a4gt0 : 0 < 4%:R × a.

Lemma deg2_poly_min x : p.[- b / (2%:R × a)] ≤ p.[x].

Lemma deg2_poly_minE : p.[- b / (2%:R × a)] = - delta / (4%:R × a).

Lemma deg2_poly_ge0 : reflect (∀ x, 0 ≤ p.[x]) (delta ≤ 0).

End Pdeg2RealConvex.

End Pdeg2Real.

Section Pdeg2RealClosed.

Variable F : rcfType.

Section Pdeg2RealClosedConvex.

Variable p : {poly F}.
Hypothesis degp : size p = 3%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let nz2 : 2%:R != 0 :> F.

Let delta := b ^+ 2 - 4%:R × a × c.

Let r1 := (- b - Num.sqrt delta) / (2%:R × a).
Let r2 := (- b + Num.sqrt delta) / (2%:R × a).

Lemma deg2_poly_factor : 0 ≤ delta → p = a *: ('X - r1%:P) × ('X - r2%:P).

End Pdeg2RealClosedConvex.

End Pdeg2RealClosed.
End Real.

End Pdeg2.

Section Degle2PolyRealConvex.

Variable (F : realFieldType) (p : {poly F}).
Hypothesis degp : (size p ≤ 3)%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let delta := b ^+ 2 - 4%:R × a × c.

Lemma deg_le2_poly_delta_ge0 : 0 ≤ a → (∀ x, 0 ≤ p.[x]) → delta ≤ 0.

End Degle2PolyRealConvex.

Section Degle2PolyRealClosedConvex.

Variable (F : rcfType) (p : {poly F}).
Hypothesis degp : (size p ≤ 3)%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let delta := b ^+ 2 - 4%:R × a × c.

Lemma deg_le2_poly_ge0 : (∀ x, 0 ≤ p.[x]) → delta ≤ 0.

End Degle2PolyRealClosedConvex.

not yet backported

Lemma deg_le2_ge0 (F : rcfType) (a b c : F) :
(∀ x, 0 ≤ a × x ^+ 2 + b × x + c)%R → (b ^+ 2 - 4%:R × a × c ≤ 0)%R.

Reserved Notation "f \min g" (at level 50, left associativity).

Definition min_fun T (R : numDomainType) (f g : T → R) x := Num.min (f x) (g x).
Notation "f \min g" := (min_fun f g) : ring_scope.
Arguments min_fun {T R} _ _ _ /.

NB: Coq 8.17.0 generalizes dependent_choice from Set to Type making the following lemma redundant

Section dependent_choice_Type.
Context X (R : X → X → Prop).

Lemma dependent_choice_Type : (∀ x, {y | R x y }) →
∀ x0, {f | f 0%N = x0 ∧ ∀ n, R (f n) (f n.+1)}.
End dependent_choice_Type.

Section max_min.
Variable R : realFieldType.
Import Num.Theory.

Let nz2 : 2%:R != 0 :> R.

Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2%:R.

Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.

End max_min.

Notation trivial := (ltac:(done)).

Section bigmax_seq.
Context d {T : orderType d} {x : T} {I : eqType}.
Variables (r : seq I) (i0 : I) (P : pred I).

NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat

Lemma le_bigmax_seq F :
i0 \in r → P i0 → (F i0 ≤ \big[Order.max/x]_(i <- r | P i) F i)%O.

NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat

Lemma bigmax_sup_seq (m : T) (F : I → T) :
i0 \in r → P i0 → (m ≤ F i0)%O →
(m ≤ \big[Order.max/x]_(i <- r | P i) F i)%O.

End bigmax_seq.
Arguments le_bigmax_seq {d T} x {I r} i0 P.

NB: PR 1079 to MathComp in progress

Lemma gerBl {R : numDomainType} (x y : R) : 0 ≤ y → x - y ≤ x.