proposition: Lemma le_map_itv_bound (x y : itv_bound int) : x <= y -> map_itv_bound (fun x => x%:~R : R) x <= map_itv_bound (fun x => x%:~R : R) y.
proof: Proof. move: x y => [xb x | []xb //=]; last by case: xb. case=> [yb y /=|//]. by rewrite /Order.le/=; case: (_ ==> _) => /=; rewrite ?ler_int// ltr_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed