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