## Stream: math-comp analysis

### Topic: ✔ Comparable ereal

#### Julien Puydt (Nov 29 2022 at 08:24):

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.


#### Cyril Cohen (Nov 29 2022 at 13:20):

1. 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)
2. If you are going to use the properties of total orders, use Import Order.Theory
3. The general theorem you are looking for is comparableT.

#### Cyril Cohen (Nov 29 2022 at 13:22):

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.