What about something along these lines?

```
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.
```

Oh, looks good! Thank you, I will use these lemmas.

abab9579 has marked this topic as resolved.

It does seem to me like e.g.

```
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).
```

could be useful. (Although the `range f`

part need to be fleshed out)

Last updated: Jan 30 2023 at 11:03 UTC