lt_(dl,dr)_set0

Author: t6s

theories/showcase/sorgenfreyline.v

@@ -200,6 +200,27 @@ case=> -[] v Ev <- /[!andbT] ->; split => //.
 by rewrite mathcomp_extra.subrKC.
 Qed.
 
+Local Lemma lt_dr_set0 x y : x < y -> dr x = set0 -> dr y = set0.
+Proof.
+move=> xy.
+rewrite !drE !(rwP eqP); apply: contraLR.
+case/set0P=> u /= [] [] v Ev <-.
+rewrite in_itv /= andbT subr_gt0 => yv.
+apply/set0P; exists (v - x) => /=.
+rewrite in_itv /= subr_gt0 (lt_trans xy yv); split => //.
+by exists v.
+Qed.
+
+Local Lemma lt_dl_set0 x y : x < y -> dl y = set0 -> dl x = set0.
+move=> xy.
+rewrite !dlE !(rwP eqP); apply: contraLR.
+case/set0P=> u /= [] [] v Ev <-.
+rewrite in_itv /= andbT addrC subr_ge0 => vx.
+apply/set0P; exists (y - v) => /=.
+rewrite in_itv /= subr_ge0 (le_trans vx (ltW xy)); split => //.
+by exists v => //; rewrite addrC.
+Qed.
+
 Lemma abs_subr_min (x y t u : R) :
   `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|.
 Proof.
@@ -381,6 +402,9 @@ have znE : z \notin E.
   by rewrite /= in_itv /= xz lexx.
 rewrite (le_lt_trans (abs_subr_min _ _ _ _)) // gt_max.
 apply/andP; split; last first.
+- rewrite /xr /zr. (dr_shift xz).
+
+
 - have drzx : dr x = [set t + (z - x) | t in dr z] by apply: dr_shift.
   rewrite /xr /zr drzx.
   have[-> | drz0] := eqVneq (dr z) set0.