proposition: Lemma predC_itv i : [predC i] =i [predU Interval -oo i.1 & Interval i.2 +oo].
proof: Proof. case: i => [a a']; move=> x; rewrite inE/= itv_splitI negb_and. by symmetry; rewrite inE/= -predC_itvl -predC_itvr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)