Lemma lem1 (A B : set R) : has_sup A -> has_sup B -> A `<=` B -> sup A <= sup B.
Proof.
by move=> [A0 ?] hsB AB; apply: le_sup => //; exact: subset_trans (@le_down _).
Qed.

Lemma subsetN (A B : set R) : A `<=` B -> -%R @` A `<=` -%R @` B.
Proof. by move=> AB _ [x Bx <-]; exists x => //; exact: AB. Qed.

Lemma lem1' (A B : set R) : has_inf A -> has_inf B -> A `<=` B -> inf B <= inf A.
Proof.
by move=> hsA hsB AB; rewrite ler_oppr opprK; apply: lem1 => //;
  [exact/has_inf_supN|exact/has_inf_supN|exact/subsetN].
Qed.

Lemma ex_image_sup_eq (f: R -> R) (A: set R) :
  {mono f : x y / x <= y} -> has_sup A -> (range f) (sup (f @` A)) -> sup (f @` A) = f (sup A).