proposition: Lemma itv_splitU c a b : a <= c <= b -> forall y, y \in Interval a b = (y \in Interval a c) || (y \in Interval c b).
proof: Proof. case/andP => leac lecb y. rewrite !itv_boundlr !(ltNge (BLeft y) _ : (BRight y <= _) = _). case: (leP a) (leP b) (leP c) => leay [] leby [] lecy //=. - by case: leP lecy (le_trans lecb leby). - by case: leP leay (le_trans leac lecy). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)