proposition: Lemma le_fpos_norm f x : fpos f x <= `|f x|.
proof: Proof. rewrite /fpos ger0_norm ?(le_maxr, lexx) //. by rewrite le_maxl normr_ge0 ler_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology