proposition: Lemma miditv_le_left i b : (i.1 < i.2)%O -> (BSide b (miditv i) <= i.2)%O.
proof: Proof. case: i => [x y] lti; have := mem_miditv lti; rewrite inE => /andP[_ ]. by apply: le_trans; rewrite !bnd_simp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)