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.
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)Import Order.Theory
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