Lemma isantisymm_leNonnegativeReals : ∏ x y : NonnegativeReals, x <= y × y <= x <-> x = y. Proof. intros x y ; split. - intros H. apply Dcuts_le_ge_eq. + now apply (pr1 H). + now apply (pr2 H). - intros ->. split ; apply isrefl_leNonnegativeReals. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.