I was stuck in one of my proofs because I couldn't compare extended real numbers correctly ; the existing `ereal_comparable`

looks pretty weak ; did I miss something obvious?

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import boolp classical_sets constructive_ereal reals.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Num.Theory Order.POrderTheory.
Open Scope real_scope.
Open Scope ring_scope.
Section Missing.
Context {R : realType}.
Check ereal_comparable. (* forall x y : \bar ?R, (0%E >=< x)%O -> (0%E >=< y)%O -> (x >=< y)%O *)
Lemma ereal_really_comparable (a b: \bar R): (a >=< b)%O.
Proof.
case: a.
- move=> a.
case: b.
+ move=>b.
by apply: real_comparable; apply: num_real.
+ by apply: le_comparable; apply: leey.
+ rewrite comparable_sym.
by apply: le_comparable; apply: leNye.
- rewrite comparable_sym.
by apply: le_comparable; apply: leey.
- by apply: le_comparable; apply: leNye.
Qed.
End Missing.
```

- Please do not use prefix
`mathcomp.analysis`

in the`From`

of`Require`

but simply`mathcomp`

(we ensure that there is no file collision in this namespace already, and we reserve the right to change a module from one submodule to another, so it's not a good idea to rely on a too precise location) - If you are going to use the properties of total orders, use
`Import Order.Theory`

- The general theorem you are looking for is
`comparableT`

.

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import constructive_ereal reals.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.Theory.
Fact ereal_really_comparable {R : realType} (a b : \bar R) : (a >=< b)%O.
Proof. exact: comparableT. Qed.
```

I realize I hadn't answered: yes, that's it! Thanks!

Julien Puydt has marked this topic as resolved.

Last updated: Nov 29 2023 at 06:01 UTC