proposition: Lemma widen_itv_subproof x i' : unify_itv i' i -> Itv.spec i' x%:inum.
proof: Proof. by move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed