proposition: Lemma isantisymm_leNonnegativeReals : ∏ x y : NonnegativeReals, x <= y × y <= x <-> x = y.
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals