proposition: Lemma le_er_map (f : R -> R) : {homo f : x y / (x <= y)%R} -> {homo er_map f : x y / x <= y}.
proof: Proof. move=> ndf. by move=> [r| |] [l| |]//=; rewrite ?leey ?leNye// !lee_fin; exact: ndf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed