proposition: Lemma subitvPr bl b1r b2r : b1r <= b2r -> {subset Interval bl b1r <= Interval bl b2r}.
proof: Proof. by move=> ?; apply: subitvP; rewrite subitvE lexx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)