fact: Definition map_itv_bound S T (f : S -> T) (b : itv_bound S) : itv_bound T := match b with | BSide b x => BSide b (f x) | BInfty b => BInfty _ b end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed