proposition: Lemma mem_miditv i : (i.1 < i.2)%O -> miditv i \in i.
proof: Proof. move: i => [[ba a|[]] [bb b|[]]] //= ab; first exact: mid_in_itv. by rewrite !in_itv -lteifBlDl subrr lteif01. by rewrite !in_itv lteifBlDr -lteifBlDl subrr lteif01. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)