proposition: Lemma predC_itvr a : [predC Interval a +oo] =i Interval -oo a.
proof: Proof. by move=> y; rewrite inE/= -predC_itvl negbK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)