proposition: Lemma le_er_map_in (A : set R) (f : R -> R) : {in A &, {homo f : x y / (x <= y)%O}} -> {in (EFin @` A)%classic &, {homo er_map f : x y / (x <= y)%E}}.
proof: Proof. move=> h x y; rewrite !inE/= => -[r Ar <-{x}] [s As <-{y}]. by rewrite !lee_fin/= => /h; apply; rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal