Lemma ispositive_apNonnegativeReals : ∏ x : NonnegativeReals, x ≠ 0 <-> 0 < x. Proof. intros X ; split. - apply sumofmaps ; [ | intros Hlt ]. + apply hinhuniv ; intros x. apply fromempty. now apply (Dcuts_zero_empty _ (pr2 (pr2 x))). + exact Hlt. - intros Hx. now right. 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.