proposition: Lemma le_fpos f1 f2 : f1 <=1 f2 -> fpos f1 <=1 fpos f2.
proof: Proof. move=> le_f x; rewrite /fpos !ger0_norm ?le_maxr ?lexx //. by rewrite le_maxl lexx /=; case: ltP => //=; rewrite le_f. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology