proposition: Lemma eq_fpos f g : f =1 g -> fpos f =1 fpos g.
proof: Proof. by move=> eq_fg x; rewrite /fpos eq_fg. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology