Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)

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]

Require Import mathcomp_extra boolp classical_sets functions.
From HB Require Import structures.

(******************************************************************************)
(* This files contains lemmas about sets and intervals.                       *)
(*                                                                            *)
(*              neitv i == the interval i is non-empty                        *)
(*                         when the support type is a numFieldType, this      *)
(*                         is equivalent to (i.1 < i.2)%O (lemma neitvE)      *)
(*   set_itv_infty_set0 == multirule to simplify empty intervals              *)
(*         conv, ndconv == convexity operator                                 *)
(*         factor a b x := (x - a) / (b - a)                                  *)
(*             set_itvE == multirule to turn intervals into inequalities      *)
(*     disjoint_itv i j == intervals i and j are disjoint                     *)
(*                                                                            *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

(* definitions and lemmas to make a bridge between MathComp intervals and     *)
(* classical sets                                                             *)
Section set_itv_porderType.
Variables (d : unit) (T : porderType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).

Definition neitv i := [set` i] != set0.

Lemma neitv_lt_bnd i : neitv i -> (i.1 < i.2)%O.
Proof.
case: i => a b; apply: contraNT => /= /itv_ge ab0.
by apply/eqP; rewrite predeqE => t; split => //=; rewrite ab0.
Qed.

Lemma set_itvP i j : [set` i] = [set` j] :> set _ <-> i =i j.
Proof.
split => [ij x|ij]; first by have /(congr1 (@^~ x))/=/is_true_inj := ij.
by rewrite predeqE => r /=; rewrite ij.
Qed.

Lemma subset_itvP i j : {subset i <= j} <-> [set` i] `<=` [set` j].
Proof. by []. Qed.

Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].
Proof. by []. Qed.

Lemma set_itvco x y : `[x, y[%classic = [set z | (x <= z < y)%O].
Proof. by []. Qed.

Lemma set_itvcc x y : `[x, y]%classic = [set z | (x <= z <= y)%O].
Proof. by []. Qed.

Lemma set_itvoc x y : `]x, y]%classic = [set z | (x < z <= y)%O].
Proof. by []. Qed.

Lemma set_itv1 x : `[x, x]%classic = [set x].
Proof. by apply/seteqP; split=> y /=; rewrite itvxx ?inE (rwP eqP). Qed.

Lemma set_itvoo0 x : `]x, x[%classic = set0.
Proof. by rewrite -subset0 => y /=; rewrite itv_ge//= bnd_simp ltxx. Qed.

Lemma set_itvoc0 x : `]x, x]%classic = set0.
Proof. by rewrite -subset0 => y /=; rewrite itv_ge//= bnd_simp ltxx. Qed.

Lemma set_itvco0 x : `[x, x[%classic = set0.
Proof. by rewrite -subset0 => y /=; rewrite itv_ge//= bnd_simp ltxx. Qed.

Lemma set_itv_infty_infty : `]-oo, +oo[%classic = @setT T.
Proof. by rewrite predeqE. Qed.

Lemma set_itv_o_infty x : `]x, +oo[%classic = [set z | (x < z)%O].
Proof. by rewrite predeqE => r /=; rewrite in_itv andbT. Qed.

Lemma set_itv_c_infty x : `[x, +oo[%classic = [set z | (x <= z)%O].
Proof. by rewrite predeqE /mkset => r; rewrite in_itv andbT. Qed.

Lemma set_itv_infty_o x : `]-oo, x[%classic = [set z | (z < x)%O].
Proof. by rewrite predeqE /mkset => r; rewrite in_itv. Qed.

Lemma set_itv_infty_c x : `]-oo, x]%classic = [set z | (z <= x)%O].
Proof. by rewrite predeqE /mkset => r; rewrite in_itv. Qed.

Lemma set_itv_pinfty_bnd a : [set` Interval +oo%O a] = set0.
Proof. by apply/eqP/negPn/negP => /neitv_lt_bnd. Qed.

Lemma set_itv_bnd_ninfty a : [set` Interval a -oo%O] = set0.
Proof. by apply/eqP/negPn/negP => /neitv_lt_bnd /=; case: a => [[]a|[]]. Qed.

Definition set_itv_infty_set0 := (set_itv_bnd_ninfty, set_itv_pinfty_bnd).

Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
  set_itvcc, set_itvoc, set_itvco, set_itv_infty_infty, set_itv_o_infty,
  set_itv_c_infty, set_itv_infty_o, set_itv_infty_c, set_itv_infty_set0).

Lemma setUitv1 (a : itv_bound T) (x : T) : (a <= BLeft x)%O ->
  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
Proof.
move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
by rewrite (rwP eqP) (rwP orP) orbC.
Qed.

Lemma setU1itv (a : itv_bound T) (x : T) : (BRight x <= a)%O ->
  x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
Proof.
move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
by rewrite (rwP eqP) (rwP orP) orbC.
Qed.

End set_itv_porderType.
Arguments neitv {d T} _.

Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
  ~~ (b1 < b2)%O -> [set` Interval b1 b2] = set0.
Proof. by move=> Nb12; rewrite -subset0 => x /=; rewrite itv_ge. Qed.

Section set_itv_latticeType.
Variables (d : unit) (T : latticeType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).

Lemma set_itvI i j :  [set` (i `&` j)%O] = [set` i] `&` [set` j].
Proof. by apply/seteqP; split=> x /=; rewrite in_itvI (rwP andP). Qed.

End set_itv_latticeType.

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

Lemma neitvE i : neitv i = (i.1 < i.2)%O.
Proof.
apply/idP/idP; first exact: neitv_lt_bnd.
by move=> /mem_miditv ii; apply/set0P; exists (miditv i).
Qed.

Lemma neitvP i : reflect (i.1 < i.2)%O (neitv i).
Proof. by apply: (iffP idP); rewrite -neitvE. Qed.

End set_itv_numFieldType.

Lemma setitv0 (R : realDomainType) : [set` (0%O : interval R)] = set0.
Proof. by rewrite predeqE. Qed.

Section interval_has_bound.
Variable R : numDomainType.

Lemma has_lbound_itv (x : R) b (a : itv_bound R) :
  has_lbound [set` Interval (BSide b x) a].
Proof. by case: b; exists x => r /andP[]; rewrite bnd_simp // => /ltW. Qed.

Lemma has_ubound_itv (x : R) b (a : itv_bound R) :
  has_ubound [set` Interval a (BSide b x)].
Proof. by case: b; exists x => r /andP[]; rewrite bnd_simp // => _ /ltW. Qed.

End interval_has_bound.

Section subr_image.
Variable R : numDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma setNK : involutive (fun E => -%R @` E).
Proof.
move=> A; rewrite image_comp (_ : _ \o _ = id) ?image_id//.
by rewrite funeqE => r /=; rewrite opprK.
Qed.

Lemma lb_ubN E x : lbound E x <-> ubound (-%R @` E) (- x).
Proof.
split=> [/lbP xlbE|/ubP xlbE].
by move=> _ [z Ez <-]; rewrite ler_oppr opprK; apply xlbE.
by move=> y Ey; rewrite -(opprK x) ler_oppl; apply xlbE; exists y.
Qed.

Lemma ub_lbN E x : ubound E x <-> lbound (-%R @` E) (- x).
Proof.
split=> [? | /lb_ubN]; first by apply/lb_ubN; rewrite opprK setNK.
by rewrite opprK setNK.
Qed.

Lemma memNE E x : E x = (-%R @` E) (- x).
Proof. by rewrite image_inj //; exact: oppr_inj. Qed.

Lemma nonemptyN E : nonempty (-%R @` E) <-> nonempty E.
Proof.
split=> [[x ENx]|[x Ex]]; exists (- x); last by rewrite -memNE.
by rewrite memNE opprK.
Qed.

Lemma opp_set_eq0 E : (-%R @` E) = set0 <-> E = set0.
Proof. by split; apply: contraPP => /eqP/set0P/nonemptyN/set0P/eqP. Qed.

Lemma has_lb_ubN E : has_lbound E <-> has_ubound (-%R @` E).
Proof.
by split=> [[x /lb_ubN] | [x /ub_lbN]]; [|rewrite setNK]; exists (- x).
Qed.

End subr_image.

Section interval_hasNbound.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma has_ubPn {E} : ~ has_ubound E <-> (forall x, exists2 y, E y & x < y).
Proof.
split; last first.
  move=> h [x] /ubP hle; case/(_ x): h => y /hle.
  by rewrite leNgt => /negbTE ->.
move/forallNP => h x; have {h} := h x.
move=> /ubP /existsNP => -[y /not_implyP[Ey /negP]].
by rewrite -ltNge => ltx; exists y.
Qed.

Lemma has_lbPn E : ~ has_lbound E <-> (forall x, exists2 y, E y & y < x).
Proof.
split=> [/has_lb_ubN /has_ubPn NEnub x|Enlb /has_lb_ubN].
  have [y ENy ltxy] := NEnub (- x); exists (- y); rewrite 1?ltr_oppl //.
  by case: ENy => z Ez <-; rewrite opprK.
apply/has_ubPn => x; have [y Ey ltyx] := Enlb (- x).
exists (- y); last by rewrite ltr_oppr.
by exists y => //; rewrite opprK.
Qed.

Lemma hasNlbound_itv (a : itv_bound R) : a != -oo%O ->
  ~ has_lbound [set` Interval -oo%O a].
Proof.
move: a => [b r|[|]] _ //.
  suff: ~ has_lbound `]-oo, r[%classic.
    by case: b => //; apply/contra_not/subset_has_lbound => x /ltW.
  apply/has_lbPn => x; exists (minr (r - 1) (x - 1)).
    by rewrite !set_itvE/= lt_minl ltr_subl_addr ltr_addl ltr01.
  by rewrite lt_minl orbC ltr_subl_addr ltr_addl ltr01.
case=> r /(_ (r - 1)) /=; rewrite in_itv /= => /(_ erefl).
by apply/negP; rewrite -ltNge ltr_subl_addr ltr_addl.
Qed.

Lemma hasNubound_itv (a : itv_bound R) : a != +oo%O ->
  ~ has_ubound [set` Interval a +oo%O].
Proof.
move: a => [b r|[|]] _ //.
  suff: ~ has_ubound `]r, +oo[%classic.
    case: b => //; apply/contra_not/subset_has_ubound => x.
    by rewrite !set_itvE => /ltW.
  apply/has_ubPn => x; rewrite !set_itvE; exists (maxr (r + 1) (x + 1));
  by rewrite ?in_itv /= ?andbT lt_maxr ltr_addl ltr01 // orbT.
case=> r /(_ (r + 1)) /=; rewrite in_itv /= => /(_ erefl).
by apply/negP; rewrite -ltNge ltr_addl.
Qed.

End interval_hasNbound.

#[global] Hint Extern 0 (has_lbound _) => solve[apply: has_lbound_itv] : core.
#[global] Hint Extern 0 (has_ubound _) => solve[apply: has_ubound_itv] : core.
#[global]
Hint Extern 0 (~ has_lbound _) => solve[by apply: hasNlbound_itv] : core.
#[global]
Hint Extern 0 (~ has_ubound _) => solve[by apply: hasNubound_itv] : core.

Lemma opp_itv_bnd_infty (R : numDomainType) (x : R) b :
  -%R @` [set` Interval (BSide b x) +oo%O] =
  [set` Interval -oo%O (BSide (negb b) (- x))].
Proof.
rewrite predeqE => /= r; split=> [[y xy <-]|xr].
  by case: b xy; rewrite !in_itv/= andbT (ler_opp2, ltr_opp2).
exists (- r); rewrite ?opprK //.
by case: b xr; rewrite !in_itv/= andbT (ler_oppr, ltr_oppr).
Qed.

Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b :
  -%R @` [set` Interval -oo%O (BSide b x)] =
  [set` Interval (BSide (negb b) (- x)) +oo%O].
Proof.
rewrite predeqE => /= r; split=> [[y xy <-]|xr].
  by case: b xy; rewrite !in_itv/= andbT (ler_opp2, ltr_opp2).
exists (- r); rewrite ?opprK //.
by case: b xr; rewrite !in_itv/= andbT (ler_oppl, ltr_oppl).
Qed.

Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) :
  -%R @` [set` Interval (BSide a x) (BSide b y)] =
  [set` Interval (BSide (~~ b) (- y)) (BSide (~~ a) (- x))].
Proof.
rewrite predeqE => /= r; split => [[{}r + <-]|].
  by rewrite !in_itv/= 2!lteif_opp2 negbK andbC.
rewrite in_itv/= negbK => yrab.
by exists (- r); rewrite ?opprK// !in_itv lteif_oppr andbC lteif_oppl.
Qed.

Lemma opp_itvoo (R : numDomainType) (x y : R) :
  -%R @` `]x, y[%classic = `](- y), (- x)[%classic.
Proof.
rewrite predeqE => /= r; split => [[{}r + <-]|].
  by rewrite !in_itv/= !ltr_opp2 andbC.
by exists (- r); rewrite ?opprK// !in_itv/= ltr_oppl ltr_oppr andbC.
Qed.

(* lemmas between itv and set-theoretic operations *)
Section set_itv_porderType.
Variables (d : unit) (T : orderType d).
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).

Lemma setCitvl a : ~` [set` Interval -oo%O a] = [set` Interval a +oo%O].
Proof. by apply/predeqP => y /=; rewrite -predC_itvl (rwP negP). Qed.

Lemma setCitvr a : ~` [set` Interval a +oo%O] = [set` Interval -oo%O a].
Proof. by rewrite -setCitvl setCK. Qed.

Lemma set_itv_splitI i : [set` i] = [set` Interval i.1 +oo%O] `&` [set` Interval -oo%O i.2].
Proof.
case: i => [a a']; apply/predeqP=> x/=.
by rewrite [in X in X <-> _]itv_splitI (rwP andP).
Qed.

Lemma setCitv i :
  ~` [set` i] = [set` Interval -oo%O i.1] `|` [set` Interval i.2 +oo%O].
Proof.
by apply/predeqP => x /=; rewrite (rwP orP) (rwP negP) [x \notin i]predC_itv.
Qed.

Lemma set_itv_splitD i :
  [set` i] = [set` Interval i.1 +oo%O] `\` [set` Interval i.2 +oo%O].
Proof. by rewrite set_itv_splitI/= setDE setCitvr. Qed.

End set_itv_porderType.

Section conv_factor_numDomainType.
Variable R : numDomainType.
Implicit Types (a b t r : R) (A : set R).

Lemma mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]).
Proof. by rewrite !in_itv/= subr_ge0 ger_addl oppr_le0 andbC. Qed.

Definition conv a b t : R := (1 - t) * a + t * b.

Lemma conv_id : conv 0 1 = id.
Proof. by apply/funext => t; rewrite /conv mulr0 add0r mulr1. Qed.

Lemma convEl a b t : conv a b t = t * (b - a) + a.
Proof. by rewrite /conv mulrBl mul1r mulrBr addrAC [RHS]addrC addrA. Qed.

Lemma convEr a b t : conv a b t = (1 - t) * (a - b) + b.
Proof.
rewrite /conv mulrBr -addrA; congr (_ + _).
by rewrite mulrBl opprB mul1r addrNK.
Qed.

Lemma conv10 t : conv 1 0 t = 1 - t.
Proof. by rewrite /conv mulr0 addr0 mulr1. Qed.

Lemma conv0 a b : conv a b 0 = a.
Proof. by rewrite /conv subr0 mul1r mul0r addr0. Qed.

Lemma conv1 a b : conv a b 1 = b.
Proof. by rewrite /conv subrr mul0r add0r mul1r. Qed.

Lemma conv_sym a b t : conv a b t = conv b a (1 - t).
Proof. by rewrite /conv opprB addrCA subrr addr0 addrC. Qed.

Lemma conv_flat a : conv a a = cst a.
Proof. by apply/funext => t; rewrite convEl subrr mulr0 add0r. Qed.

Lemma leW_conv a b : a <= b -> {homo conv a b : x y / x <= y}.
Proof. by move=> ? ? ? ?; rewrite !convEl ler_add ?ler_wpmul2r// subr_ge0. Qed.

Definition factor a b x := (x - a) / (b - a).

Lemma leW_factor a b : a <= b -> {homo factor a b : x y / x <= y}.
Proof.
by move=> ? ? ? ?; rewrite /factor ler_wpmul2r ?ler_add// invr_ge0 subr_ge0.
Qed.

Lemma factor_flat a : factor a a = cst 0.
Proof. by apply/funext => x; rewrite /factor subrr invr0 mulr0. Qed.

Lemma factorl a b : factor a b a = 0.
Proof. by rewrite /factor subrr mul0r. Qed.

Definition ndconv a b of a < b := conv a b.

Lemma ndconvE a b (ab : a < b) : ndconv ab = conv a b. Proof. by []. Qed.

End conv_factor_numDomainType.

Section conv_factor_numFieldType.
Variable R : numFieldType.
Implicit Types (a b t r : R) (A : set R).

Lemma factorr a b : a != b -> factor a b b = 1.
Proof. by move=> Nab; rewrite /factor divff// subr_eq0 eq_sym. Qed.

Lemma factorK a b : a != b -> cancel (factor a b) (conv a b).
Proof. by move=> ? x; rewrite convEl mulfVK ?addrNK// subr_eq0 eq_sym. Qed.

Lemma convK a b : a != b -> cancel (conv a b) (factor a b).
Proof. by move=> ? x; rewrite /factor convEl addrK mulfK// subr_eq0 eq_sym. Qed.

Lemma conv_inj a b : a != b -> injective (conv a b).
Proof. by move/convK/can_inj. Qed.

Lemma factor_inj a b : a != b -> injective (factor a b).
Proof. by move/factorK/can_inj. Qed.

Lemma conv_bij a b : a != b -> bijective (conv a b).
Proof. by move=> ab; apply: Bijective (convK ab) (factorK ab). Qed.

Lemma factor_bij a b : a != b -> bijective (factor a b).
Proof. by move=> ab; apply: Bijective (factorK ab) (convK ab). Qed.

Lemma le_conv a b : a < b -> {mono conv a b : x y / x <= y}.
Proof.
move=> ltab; have leab := ltW ltab.
by apply: homo_mono (convK _) (leW_factor _) (leW_conv _); rewrite // lt_eqF.
Qed.

Lemma le_factor a b : a < b -> {mono factor a b : x y / x <= y}.
Proof.
move=> ltab; have leab := ltW ltab.
by apply: homo_mono (factorK _) (leW_conv _) (leW_factor _); rewrite // lt_eqF.
Qed.

Lemma lt_conv a b : a < b -> {mono conv a b : x y / x < y}.
Proof. by move/le_conv/leW_mono. Qed.

Lemma lt_factor a b : a < b -> {mono factor a b : x y / x < y}.
Proof. by move/le_factor/leW_mono. Qed.

Let ltNeq a b : a < b -> a != b. Proof. by move=> /lt_eqF->. Qed.

HB.instance Definition _ a b (ab : a < b) :=
  @Can2.Build _ _ setT setT (ndconv ab) (factor a b)
    (fun _ _ => I) (fun _ _ => I)
    (in1W (convK (ltNeq ab))) (in1W (factorK (ltNeq ab))).

Lemma conv_itv_bij ba bb a b : a < b ->
  set_bij [set` Interval (BSide ba 0) (BSide bb 1)]
          [set` Interval (BSide ba a) (BSide bb b)] (conv a b).
Proof.
move=> ltab; rewrite -ndconvE; apply: bij_subr => //=; rewrite setTI ?ndconvE.
apply/predeqP => t /=; rewrite !in_itv/= {1}convEl convEr.
rewrite -lteif_subl_addr subrr -lteif_pdivr_mulr ?subr_gt0// mul0r.
rewrite -lteif_subr_addr subrr -lteif_ndivr_mulr ?subr_lt0// mul0r.
by rewrite lteif_subr_addl addr0.
Qed.

Lemma factor_itv_bij ba bb a b : a < b ->
  set_bij [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).
Proof.
move=> ltab; have -> : factor a b = (ndconv ltab)^-1%FUN by [].
by apply/splitbij_sub_sym => //; apply: conv_itv_bij.
Qed.

Lemma mem_conv_itv ba bb a b : a < b ->
  set_fun [set` Interval (BSide ba 0) (BSide bb 1)]
          [set` Interval (BSide ba a) (BSide bb b)] (conv a b).
Proof. by case/(conv_itv_bij ba bb). Qed.

Lemma mem_conv_itvcc a b : a <= b -> set_fun `[0, 1] `[a, b] (conv a b).
Proof.
rewrite le_eqVlt => /predU1P[<-|]; first by rewrite set_itv1 conv_flat.
by move=> lt_ab; case: (conv_itv_bij true false lt_ab).
Qed.

Lemma range_conv ba bb a b : a < b ->
   conv a b @` [set` Interval (BSide ba 0) (BSide bb 1)] =
               [set` Interval (BSide ba a) (BSide bb b)].
Proof. by move=> /(conv_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed.

Lemma range_factor ba bb a b : a < b ->
   factor a b @` [set` Interval (BSide ba a) (BSide bb b)] =
                 [set` Interval (BSide ba 0) (BSide bb 1)].
Proof. by move=> /(factor_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed.

End conv_factor_numFieldType.

Lemma mem_factor_itv (R : realFieldType) ba bb (a b : R) :
  set_fun [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).
Proof.
have [|leba] := ltP a b; first by case/(factor_itv_bij ba bb).
move=> x /=; have [|/itv_ge->//] := (boolP (BSide ba a < BSide bb b)%O).
rewrite lteBSide; case: ba bb => [] []//=; rewrite ?le_gtF//.
by case: ltgtP leba => // -> _ _ _; rewrite factor_flat in_itv/= lexx ler01.
Qed.

Lemma neitv_bnd1 (R : numFieldType) (s : seq (interval R)) :
  all neitv s -> forall i, i \in s -> i.1 != +oo%O.
Proof.
move=> /allP sne [a b] si /=; apply/negP => /eqP boo; move: si.
by rewrite boo => /sne /negP; apply; rewrite set_itv_infty_set0.
Qed.

Lemma neitv_bnd2 (R : numFieldType) (s : seq (interval R)) :
  all neitv s -> forall i, i \in s -> i.2 != -oo%O.
Proof.
move=> /allP sne [a b] si /=; apply/negP => /eqP boo; move: si.
by rewrite boo => /sne /negP; apply; rewrite set_itv_infty_set0.
Qed.

Lemma trivIset_set_itv_nth (R : numDomainType) def (s : seq (interval R))
  (D : set nat) : [set` def] = set0 ->
  trivIset D (fun i => [set` nth def s i]) <->
    trivIset D (fun i => nth set0 [seq [set` j] | j <- s] i).
Proof.
move=> def0; split=> /trivIsetP ss; apply/trivIsetP => i j Di Dj ij.
- have [si|si] := ltP i (size s); last first.
    by rewrite (nth_default set0) ?size_map// set0I.
  have [sj|sj] := ltP j (size s); last first.
    by rewrite setIC (nth_default set0) ?size_map// set0I.
  by rewrite (nth_map def) // (nth_map def) // ss.
- have [?|h] := ltP i (size s); last by rewrite (nth_default def h) def0 set0I.
  have [?|h] := ltP j (size s); last by rewrite (nth_default def h) def0 setI0.
  by have := ss _ _ Di Dj ij; rewrite (nth_map def) // (nth_map def).
Qed.
Arguments trivIset_set_itv_nth {R} _ {s}.

Section disjoint_itv.
Context {R : numDomainType}.

Definition disjoint_itv : rel (interval R) :=
  fun a b => [disjoint [set` a] & [set` b]].

Lemma disjoint_itvxx (i : interval R) : neitv i -> ~~ disjoint_itv i i.
Proof. by move=> i0; rewrite /disjoint_itv/= /disj_set /= setIid. Qed.

Lemma lt_disjoint (i j : interval R) :
  (forall x y, x \in i -> y \in j -> x < y) -> disjoint_itv i j.
Proof.
move=> ij; apply/eqP; rewrite predeqE => x; split => // -[xi xj].
by have := ij _ _ xi xj; rewrite ltxx.
Qed.

End disjoint_itv.

Lemma disjoint_neitv {R : realFieldType} (i j : interval R) :
  disjoint_itv i j <-> ~~ neitv (itv_meet i j).
Proof.
case: i j => [a b] [c d]; rewrite /disjoint_itv/disj_set /= -set_itvI.
by split => [/negPn//|?]; apply/negPn.
Qed.