proposition: Lemma gt0_funenegM r f : (0 < r)%R -> (fun x => r%:E * f x)^\- = (fun x => r%:E * (f^\- x)).
proof: Proof. by move=> r0; rewrite funeqE => x; rewrite /funeneg -muleN 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