proposition: Lemma subset_itv (r s u v : bool) x y : r <= u -> v <= s -> {subset Interval (BSide r x) (BSide s y) <= Interval (BSide u x) (BSide v y)}.
proof: Proof. by move: r s u v=> [] [] [] []// *; apply: subitvP; rewrite subitvE !bound_lexx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)