Lemma hr_to_NR_nonpositive : ∏ x : hr_commring, (hr_to_NRpos x = 0) <-> hr_le_rel x 0%ring. Proof. intros x. pattern x at 2. rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero. unfold hr_to_NRpos. split. - change (hr_to_NR x) with (pr1 (hr_to_NR x),,pr2 _). simpl pr1 ; simpl pr2 ; intros ->. apply NR_to_hr_le ; simpl. rewrite !islunit_zero_plusNonnegativeReals. now apply isnonnegative_NonnegativeReals. - pattern x at 2. rewrite <- (hr_to_NR_bij x). generalize (hr_to_NR x) ; clear x ; intros x Hx. unfold hr_to_NR, NR_to_hr. rewrite setquotunivcomm ; simpl. apply_pr2_in NR_to_hr_le Hx. rewrite isrunit_zero_plusNonnegativeReals, islunit_zero_plusNonnegativeReals in Hx. now apply minusNonnegativeReals_eq_zero. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.