proposition: Lemma fneg_natrM f (n : T -> nat) x : fneg (fun x => (n x)%:R * f x) x = (n x)%:R * fneg f x.
proof: Proof. rewrite -[in RHS]fposN -fpos_natrM -fposN. by apply/eq_fpos=> y; rewrite mulrN. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology