proposition: Lemma ispositive_apNonnegativeReals : ∏ x : NonnegativeReals, x ≠ 0 <-> 0 < x.
proof: 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.
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