Compatible with MathComp master (and hopefully 1.12)

config.nix

@@ -1,6 +1,6 @@
 {
   coq = "8.11";
-  mathcomp = "mathcomp-1.11.0";
-  mathcomp-real-closed = "1.1.1";
-  mathcomp-finmap = "1.5.0";
+  mathcomp = "mathcomp-1.12.0";
+  mathcomp-real-closed = "1.1.2";
+  mathcomp-finmap = "1.5.1";
 }

theories/derive.v

@@ -1312,7 +1312,7 @@ Proof.
 move=> leab fcont; set imf := [set t | (f @` [set x | x \in `[a, b]]) t].
 have imf_sup : has_sup imf.
   split.
-    by exists (f a) => //; rewrite /imf; apply/imageP; rewrite /= inE /= lexx.
+    by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` [set x | x \in `[a, b]] : set R^o).
     apply/compact_bounded/continuous_compact; last exact: segment_compact.
     by move=> ?; rewrite inE => /fcont.
@@ -1430,9 +1430,9 @@ apply/eqP; rewrite eq_le; apply/andP; split.
     by rewrite invr_ge0; apply: ltW; near: h; exists 1.
   rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
   exists (b - c); first by rewrite /= subr_gt0 (itvP cab).
-  move=> h; rewrite /= distrC subr0.
-  move=> /(le_lt_trans (ler_norm _)); rewrite ltr_subr_addr inE/= => ->.
-  by move=> /ltr_spsaddl -> //; rewrite (itvP cab).
+  move=> h; rewrite /= distrC subr0 /= in_itv /= -ltr_subr_addr.
+  move=> /(le_lt_trans (ler_norm _)) -> /ltr_spsaddl -> //.
+  by rewrite (itvP cab).
 rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl.
 apply: le0r_cvg_map; last first.
   have /fdrvbl dfc := cab; rewrite -(@cvg_at_leftE _ _ (fun h => h^-1 *: ((f \o shift c) _ - f c))) //.
@@ -1444,7 +1444,7 @@ near=> h; apply: mulr_le0.
 rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
 exists (c - a); first by rewrite /= subr_gt0 (itvP cab).
 move=> h; rewrite /= distrC subr0.
-move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl inE/= => -> _.
+move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl in_itv /= => -> _.
 by move=> /ltr_snsaddl -> //; rewrite (itvP cab).
 Grab Existential Variables. all: end_near. Qed.
 
@@ -1471,24 +1471,24 @@ case: (pselect ([set a; b] cmax))=> [cmaxeaVb|]; last first.
   move=> /asboolPn; rewrite asbool_or => /norP.
   move=> [/asboolPn/eqP cnea /asboolPn/eqP cneb].
   have {}cmaxab : cmax \in `]a, b[.
-    by rewrite inE/= !lt_def !(itvP cmaxab) cnea eq_sym cneb.
+    by rewrite in_itv /= !lt_def !(itvP cmaxab) cnea eq_sym cneb.
   exists cmax => //; apply: derive1_at_max (ltW ltab) fdrvbl cmaxab _ => t tab.
-  by apply: fcmax; rewrite inE/= !ltW // (itvP tab).
+  by apply: fcmax; rewrite in_itv /= !ltW // (itvP tab).
 have [cmin cminab fcmin] := EVT_min (ltW ltab) fcont.
 case: (pselect ([set a; b] cmin))=> [cmineaVb|]; last first.
   move=> /asboolPn; rewrite asbool_or => /norP.
   move=> [/asboolPn/eqP cnea /asboolPn/eqP cneb].
   have {}cminab : cmin \in `]a, b[.
-    by rewrite inE/= !lt_def !(itvP cminab) cnea eq_sym cneb.
+    by rewrite in_itv /= !lt_def !(itvP cminab) cnea eq_sym cneb.
   exists cmin => //; apply: derive1_at_min (ltW ltab) fdrvbl cminab _ => t tab.
-  by apply: fcmin; rewrite inE/= !ltW // (itvP tab).
+  by apply: fcmin; rewrite in_itv /= !ltW // (itvP tab).
 have midab : (a + b) / 2 \in `]a, b[ by apply: mid_in_itvoo.
 exists ((a + b) / 2) => //; apply: derive1_at_max (ltW ltab) fdrvbl (midab) _.
 move=> t tab.
 suff fcst : forall s, s \in `]a, b[ -> f s = f cmax by rewrite !fcst.
 move=> s sab.
-apply/eqP; rewrite eq_le fcmax; last by rewrite inE/= !ltW ?(itvP sab).
-suff -> : f cmax = f cmin by rewrite fcmin // inE/= !ltW ?(itvP sab).
+apply/eqP; rewrite eq_le fcmax; last by rewrite in_itv /= !ltW ?(itvP sab).
+suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(itvP sab).
 by case: cmaxeaVb => ->; case: cmineaVb => ->.
 Qed.
 
@@ -1512,7 +1512,7 @@ have gaegb : g a = g b.
     by rewrite mul1r addrCA subrr addr0.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
-exists c; first by apply/andP; split; apply/ltW; rewrite (itvP cab).
+exists c; first by rewrite in_itv /= ltW (itvP cab).
 have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //; last first.
   exact/derivable1_diffP.
 move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0.
@@ -1526,7 +1526,8 @@ Lemma ler0_derive1_nincr (R : realType) (f : R^o -> R^o) (a b : R) :
   forall x y, a <= x -> x <= y -> y <= b -> f y <= f x.
 Proof.
 move=> fdrvbl dfle0 x y leax lexy leyb; rewrite -subr_ge0.
-have itvW : {subset `[x, y] <= `[a, b]} by apply/subitvP; rewrite /= leyb leax.
+have itvW : {subset `[x, y] <= `[a, b]}.
+  by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
 have fdrv z : z \in `]x, y[ -> is_derive (z : R^o) 1 f (f^`()z).
   rewrite inE => /andP [/ltW lexz /ltW lezy].
   apply: DeriveDef; last by rewrite derive1E.

theories/normedtype.v

@@ -329,10 +329,9 @@ Lemma in_segment_addgt0Pr (R : numFieldType) (x y z : R) :
   reflect (forall e, e > 0 -> y \in `[(x - e), (z + e)]) (y \in `[x, z]).
 Proof.
 apply/(iffP idP)=> [xyz _/posnumP[e] | xyz_e].
-  rewrite inE/=; apply/andP; split; last by rewrite ler_paddr // (itvP xyz).
-  by rewrite ler_subl_addr ler_paddr // (itvP xyz).
-rewrite inE/=; apply/andP.
-by split; apply/ler_addgt0Pr => ? /xyz_e /andP /= []; rewrite ler_subl_addr.
+  by rewrite in_itv /= ler_subl_addr !ler_paddr // (itvP xyz).
+by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e;
+  rewrite in_itv /= ler_subl_addr => /andP [].
 Qed.
 
 Lemma in_segment_addgt0Pl (R : numFieldType) (x y z : R) :
@@ -1033,7 +1032,7 @@ Lemma Rhausdorff (R : realFieldType) : hausdorff [topologicalType of R^o].
 Proof.
 move=> x y clxy; apply/eqP; rewrite eq_le.
 apply/(@in_segment_addgt0Pr _ x _ x) => _ /posnumP[e].
-rewrite inE -ler_distl; set he := (e%:num / 2)%:pos.
+rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos.
 have [z []] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he).
 move=> zx_he yz_he.
 rewrite -(subrKA z) (le_trans (ler_norm_add _ _) _)// ltW //.
@@ -2253,37 +2252,32 @@ rewrite [X in closed X](_ : (eq^~ _) = ~` (xpredC (eq_op^~ y))).
 by rewrite predeqE /setC => x /=; rewrite (rwP eqP); case: eqP; split.
 Qed.
 
-(* TODO: move after rebase on mathcomp 1.12?  *)
-Definition isBOpen (b : itv_bound R) :=
-  if b is BOpen _ then true else false.
+Definition bound_side d (T : porderType d) (c : bool) (x : itv_bound T) :=
+  if x is BSide c' _ then c == c' else false.
 
-Definition isBClosed (b : itv_bound R) :=
-  if b is BOpen_if false _ then true else false.
-
-Lemma interval_open a b : ~~ isBClosed a -> ~~ isBClosed b ->
+Lemma interval_open a b : ~~ bound_side true a -> ~~ bound_side false b ->
   open [set x : R^o | x \in Interval a b].
 Proof.
-move: a b => [[]//a|] [[]//b|] _ _.
+move: a b => [[]a|[]] [[]b|[]]// _ _.
 - have -> : [set x | a < x < b] = [set x | a < x] `&` [set x | x < b].
     by rewrite predeqE => r; rewrite /mkset; split => [/andP[? ?] //|[-> ->]].
   by apply openI; [exact: open_gt | exact: open_lt].
-- rewrite (_ : [set x | x \in _] = [set x : R^o | x > a]) //.
-  by rewrite predeqE => r; split => //; rewrite /mkset ?(inE,lersifT,andbT).
+- by under eq_set do rewrite itv_ge// inE.
+- by under eq_set do rewrite in_itv andbT/=; exact: open_gt.
 - exact: open_lt.
 - by rewrite (_ : mkset _ = setT); [exact: openT | rewrite predeqE].
 Qed.
 
-Lemma interval_closed a b : ~~ isBOpen a -> ~~ isBOpen b ->
+Lemma interval_closed a b : ~~ bound_side false a -> ~~ bound_side true b ->
   closed [set x : R^o | x \in Interval a b].
 Proof.
-move: a b => [[]//a|] [[]//b|] _ _.
+move: a b => [[]a|[]] [[]b|[]]// _ _;
+  do ?by under eq_set do rewrite itv_ge// inE falseE; apply: closed0.
 - have -> : [set x | x \in `[a, b]] = [set x | x >= a] `&` [set x | x <= b].
-    by rewrite predeqE => ?; rewrite /= inE; split=> [/andP [] | /= [->]].
+    by rewrite predeqE => ?; rewrite /= in_itv/=; split=> [/andP[]|[->]].
   by apply closedI; [exact: closed_ge | exact: closed_le].
-- rewrite (_ : mkset _ = [set x : R^o | x >= a]); first exact :closed_ge.
-  by rewrite predeqE => r; split => //; rewrite /mkset ?(inE,lersifT,andbT).
+- by under eq_set do rewrite in_itv andbT/=; exact: closed_ge.
 - exact: closed_le.
-- by rewrite (_ : mkset _ = setT); [exact: closedT|rewrite predeqE].
 Qed.
 
 End open_closed_sets.
@@ -2348,16 +2342,9 @@ Qed.
 
 Lemma interval_is_interval (i : interval R) : is_interval [set x | x \in i].
 Proof.
-move: i => [[[] i|] [[] j|]] //= x y; rewrite /mkset !(inE,lersifT,lersifF);
-  move=> /andP[ax ?] /andP[? yb] z /andP[? ?]; rewrite !(inE,lersifT,lersifF).
-by rewrite (lt_trans ax) // (lt_trans _ yb).
-by rewrite (lt_trans ax) // (le_trans (ltW _) yb).
-by rewrite (lt_trans ax).
-by rewrite (le_trans ax (ltW _)) // (lt_trans _ yb).
-by rewrite (le_trans ax (ltW _)) // (le_trans (ltW _) yb).
-by rewrite (le_trans ax (ltW _)).
-by rewrite (lt_trans _ yb).
-by rewrite (le_trans (ltW _) yb).
+by case: i => -[[]a|[]] [[]b|[]] // x y /=; do ?[by rewrite ?itv_ge//];
+   move=> xi yi z; rewrite -[x < z < y]/(z \in `]x, y[); apply/subitvP;
+   rewrite subitvE /Order.le/= ?(itvP xi, itvP yi).
 Qed.
 
 End interval.
@@ -2447,7 +2434,7 @@ Proof.
 move=> iX bX aX; rewrite eqEsubset; split=> [r Xr|].
   apply/andP; split;
     [exact: left_bounded_interior|exact: right_bounded_interior].
-rewrite -open_subsetE; last exact: (@interval_open _ (BOpen _) (BOpen _)).
+rewrite -open_subsetE; last exact: (@interval_open _ (BRight _) (BLeft _)).
 move=> r /andP[iXr rsX].
 have [/set0P X0|/negPn/eqP X0] := boolP (X != set0); last first.
   by move: (lt_trans iXr rsX); rewrite X0 inf_out ?sup_out ?ltxx // => - [[]].
@@ -2459,64 +2446,59 @@ have /(sup_adherent hsX)[f Xf] : 0 < sup X - r by rewrite subr_gt0.
 by rewrite opprB addrCA subrr addr0 => rf; apply: (iX _ _ Xe Xf); rewrite er rf.
 Qed.
 
-Definition interval_of_set (X : set R) : interval R :=
-  match `[< has_lbound X >], `[< has_ubound X >] with
-  | false, false => `]-oo, +oo[
-  | true , false => if `[< X (inf X) >] then `[inf X, +oo[ else `]inf X, +oo[
-  | false, true  => if `[< X (sup X) >] then `]-oo, sup X] else `]-oo, (sup X)[
-  | true , true  => if `[< X (inf X) >] then
-      (if `[< X (sup X) >] then `[inf X, sup X] else `[inf X, (sup X)[)
-    else
-      (if `[< X (sup X) >] then `]inf X, sup X] else `]inf X, (sup X)[)
-  end.
-
-Lemma is_intervalP (X : set R) :
-  is_interval X <-> exists i : interval R, X = [set x | x \in i].
-Proof.
-split=> [iX|[i ->]]; last exact: interval_is_interval.
-exists (interval_of_set X); rewrite predeqE => x; split => [Xx|];
-    rewrite /mkset inE /interval_of_set /=.
-- case: ifPn => /asboolP ?; case: ifPn => /asboolP ? //.
-  + by case: ifPn => /asboolP ?; case: ifPn => /asboolP ?;
-      rewrite !(lersifF,lersifT,sup_ub,inf_lb,sup_ub_strict,inf_lb_strict).
-  + case: ifPn => /asboolP XinfX; rewrite !(lersifF,lersifT);
-      by [rewrite inf_lb | rewrite inf_lb_strict].
-  + case: ifPn => /asboolP XsupX; rewrite !(lersifF,lersifT);
-      by [rewrite sup_ub | rewrite sup_ub_strict].
-- case: ifPn => /asboolP ?; case: ifPn => /asboolP ?.
-  + case: ifPn => /asboolP XinfX; case: ifPn => /asboolP XsupX;
-      rewrite !(lersifF,lersifT).
-    * move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx].
-      rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
-      apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_bounded_interior // /mkset infXx.
-    * move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx supXx].
-      apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_bounded_interior // /mkset infXx.
-    * move=> /andP[infXx]; rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
-      apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_bounded_interior // /mkset infXx.
-    * move=> ?; apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_bounded_interior // /mkset infXx.
-  + case: ifPn => /asboolP XinfX; rewrite !(lersifF,lersifT,andbT).
-    * rewrite le_eqVlt => /orP[/eqP<-//|infXx].
-      apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_right_unbounded_interior.
-    * move=> infXx; apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_right_unbounded_interior.
-  + case: ifPn => /asboolP XsupX /=.
-    * rewrite le_eqVlt => /orP[/eqP->//|xsupX].
-      apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_left_unbounded_interior.
-    * move=> xsupX; apply: (@interior_subset [topologicalType of R^o]).
-      by rewrite interval_left_unbounded_interior.
-  + by move=> _; rewrite (interval_unbounded_setT iX).
-Qed.
-
-End interval_realType.
-
-Lemma connected_intervalP (R : realType) (E : set R^o) :
-  connected E <-> is_interval E.
+Definition Rhull (X : set R) : interval R := Interval
+  (if `[< has_lbound X >] then BSide `[< X (inf X) >] (inf X)
+                          else BInfty _ true)
+  (if `[< has_ubound X >] then BSide (~~ `[< X (sup X) >]) (sup X)
+                          else BInfty _ false).
+
+Lemma sub_Rhull (X : set R) : X `<=` [set x | x \in Rhull X].
+Proof.
+move=> x Xx/=; rewrite in_itv/=.
+case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
++ by case: asboolP => ?; case: asboolP => ? //=;
+     rewrite !(lteifF, lteifT, sup_ub, inf_lb, sup_ub_strict, inf_lb_strict).
++ by case: asboolP => XinfX; rewrite !(lteifF, lteifT);
+     [rewrite inf_lb | rewrite inf_lb_strict].
++ by case: asboolP => XsupX; rewrite !(lteifF, lteifT);
+     [rewrite sup_ub | rewrite sup_ub_strict].
+Qed.
+
+Lemma is_intervalP (X : set R) : is_interval X <-> X = [set x | x \in Rhull X].
+Proof.
+split=> [iX|->]; last exact: interval_is_interval.
+rewrite predeqE => x /=; split; [exact: sub_Rhull | rewrite in_itv/=].
+case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
+- case: asboolP => XinfX; case: asboolP => XsupX;
+    rewrite !(lteifF, lteifT).
+  + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx].
+    rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
+    apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_bounded_interior // /mkset infXx.
+  + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx supXx].
+    apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_bounded_interior // /mkset infXx.
+  + move=> /andP[infXx]; rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
+    apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_bounded_interior // /mkset infXx.
+  + move=> ?; apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_bounded_interior // /mkset infXx.
+- case: asboolP => XinfX; rewrite !(lteifF, lteifT, andbT).
+  + rewrite le_eqVlt => /orP[/eqP<-//|infXx].
+    apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_right_unbounded_interior.
+  + move=> infXx; apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_right_unbounded_interior.
+- case: asboolP => XsupX /=.
+  + rewrite le_eqVlt => /orP[/eqP->//|xsupX].
+    apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_left_unbounded_interior.
+  + move=> xsupX; apply: (@interior_subset [topologicalType of R^o]).
+    by rewrite interval_left_unbounded_interior.
+- by move=> _; rewrite (interval_unbounded_setT iX).
+Qed.
+
+Lemma connected_intervalP (E : set R^o) : connected E <-> is_interval E.
 Proof.
 split => [cE x y Ex Ey z /andP[xz zy]|].
 - apply: contrapT => Ez.
@@ -2535,8 +2517,9 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
   wlog xy : A A0 EU sepA x A0x y A1y / x < y.
     move=> /= wlog_hypo; have [xy|yx|{wlog_hypo}yx] := ltgtP x y.
     + exact: (wlog_hypo _ _ _ _ _ A0x _ A1y).
-    + apply: (wlog_hypo (A \o negb) _ _ _ y _ x) => //=;
+    + apply: (wlog_hypo (A \o negb) _ _ _ y _ x) => //=.
         by [rewrite setUC | rewrite separatedC].
+        by rewrite separatedC.
     + move/separated_disjoint : sepA; rewrite predeqE => /(_ x)[] + _; apply.
       by split => //; rewrite yx.
   pose z := sup (A false `&` [set z | x <= z <= y]).
@@ -2582,6 +2565,7 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
     by split => //; rewrite /mkset /z1 (le_trans xz) /= ?ler_addl // (ltW z1y).
   by rewrite EU => -[//|]; apply: contra_not ncA1z1; exact: subset_closure.
 Qed.
+End interval_realType.
 
 Section segment.
 Variable R : realType.
@@ -2615,7 +2599,7 @@ apply: segment_connected.
   rewrite openE => /(_ _ fx) [e egt0 xe_fi]; exists e => // y xe_y.
   exists D' => //; split; last by exists i => //; apply/xe_fi.
   move=> z /= ayz; case: (lerP z x) => [lezx|ltxz].
-    by apply/saxUf; rewrite /= inE/= (itvP ayz) lezx.
+    by apply/saxUf; rewrite /= in_itv/= (itvP ayz) lezx.
   exists i => //; apply/xe_fi; rewrite /ball_/= distrC ger0_norm.
     have lezy : z <= y by rewrite (itvP ayz).
     rewrite ltr_subl_addl; apply: le_lt_trans lezy _; rewrite -ltr_subl_addr.
@@ -2632,7 +2616,7 @@ split=> [z axz|]; last first.
   exists i; first by rewrite /= !inE eq_refl.
   by apply/xe_fi; rewrite /ball_/= subrr normr0.
 case: (lerP z y) => [lezy|ltyz].
-  have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite inE/= (itvP axz) lezy.
+  have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite in_itv /= (itvP axz) lezy.
   by exists j => //=; rewrite inE orbC Dj.
 exists i; first by rewrite /= !inE eq_refl.
 apply/xe_fi; rewrite /ball_/= ger0_norm; last first.
@@ -2666,9 +2650,9 @@ move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
     by move=> x /fcont; apply: (@continuousN _ [normedModType R of R^o]).
   by rewrite ler_oppr opprK ler_oppr opprK andbC.
 move=> /andP[]; rewrite le_eqVlt => /orP [/eqP<- _|ltfav].
-  by exists a => //; rewrite inE/= lexx leab.
+  by exists a => //; rewrite in_itv /= lexx leab.
 rewrite le_eqVlt => /orP [/eqP->|ltvfb].
-  by exists b => //; rewrite inE/= lexx leab.
+  by exists b => //; rewrite in_itv /= lexx leab.
 set A := [set c | (c <= b) && (f c <= v)].
 have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW.
 have supA : has_sup A by split=> //; exists b; apply/ubP => ? /andP [].
@@ -2703,8 +2687,8 @@ rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t.
     by move: lefsupv; rewrite leNgt -besup ltvfb.
   move=> t lttb ltsupt; move: lttb; rewrite /= distrC.
   by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltW.
-move=> t /andP [ltsupt /= letb]; rewrite ltNge; apply/negP => leftv.
-move: ltsupt => /=; rewrite ltNge => /negP; apply.
+move=> t; rewrite in_itv /=; case/andP => ltsupt letb.
+apply/contra_lt: ltsupt => leftv.
 by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leftv letb.
 Grab Existential Variables. all: end_near. Qed.