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.