proposition: Lemma ge0_fneg f x : 0 <= fneg f x.
proof: Proof. by apply/normr_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology