proposition: Lemma itv_top_typ_subproof (R : numDomainType) (x : R) : Itv.spec `]-oo, +oo[ x.
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed