proposition: Lemma gt0_funeposM r f : (0 < r)%R -> (fun x => r%:E * f x)^\+ = (fun x => r%:E * (f^\+ x)).
proof: Proof. by move=> ?; rewrite funeqE => x; rewrite /funepos maxeMr// mule0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences