proposition: Lemma fpos_natrM f (n : T -> nat) x : fpos (fun x => (n x)%:R * f x) x = (n x)%:R * fpos f x.
proof: Proof. rewrite /fpos -[in RHS]normr_nat -normrM. by rewrite maxr_pMr ?ler0n // mulr0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology