proposition: Lemma itv_joinKI i2 i1 : itv_meet i1 (itv_join i1 i2) = i1.
proof: Proof. by case: i1 i2 => [? ?][? ?] /=; rewrite meetKU joinKI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)