proposition: Lemma fpos_ge0 f x : (forall x, 0 <= f x ) -> fpos f x = f x.
proof: Proof. by move=> ?; rewrite /fpos max_r ?ger0_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology