proposition: Lemma map_itv_bound_min (x y : itv_bound int) : Itv.map_itv_bound (fun x => x%:~R : R) (Order.min x y) = Order.min (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y).
proof: Proof. have [lexy|ltyx] := leP x y; first by rewrite !minEle Itv.le_map_itv_bound. by rewrite minElt -if_neg -leNgt Itv.le_map_itv_bound // ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed