proposition: Lemma le1 x : unify_itv `]-oo, Posz 1] i -> x%:inum <= 1%R :> R.
proof: Proof. move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). by rewrite in_itv/=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed