proposition: Lemma lt0_funeposM r f : (r < 0)%R -> (fun x => r%:E * f x)^\+ = (fun x => - r%:E * (f^\- x)).
proof: Proof. move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite EFinN mulNe. by rewrite funeposN gt0_funenegM -1?ltrNr ?oppr0. 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