proposition: Lemma ereal_comparable x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (x >=< y)%O.
proof: Proof. move: x y => [x||] [y||] //; rewrite /Order.comparable !lee_fin -!realE. - exact: real_comparable. - by rewrite /lee/= => ->. - by rewrite /lee/= => _ ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed