proposition: Lemma boundr_in_itv c x b : x \in Interval b (BSide c x) = ~~ c && (b <= BLeft x).
proof: Proof. by rewrite itv_boundlr bound_lexx implybF andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)