fact: Definition map_itv S T (f : S -> T) (i : interval S) : interval T := let 'Interval l u := i in Interval (map_itv_bound f l) (map_itv_bound f u).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed