proposition: Lemma subitv_map_itv (x y : interval int) : x <= y -> map_itv (fun x => x%:~R : R) x <= map_itv (fun x => x%:~R : R) y.
proof: Proof. move: x y => [lx ux] [ly uy] /andP[lel leu]. apply/andP; split; exact: le_map_itv_bound. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed