proposition: Lemma lteif_in_itv cl cr yl yr x : x \in Interval (BSide cl yl) (BSide cr yr) -> yl < yr ?<= if cl && ~~ cr.
proof: Proof. exact: lt_in_itv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)