proposition: Lemma itv_dec : forall x i, reflect (itv_decompose i x) (x \in i).
proof: Proof. by move=> ? [[? ?|[]][? ?|[]]]; apply: (iffP andP); case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)