proposition: Lemma hr_to_NR_nonnegative : ∏ x : hr_commring, (hr_to_NRneg x = 0) <-> hr_le_rel 0%ring x.
proof: 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_NRneg. split. - generalize (hr_to_NR x). intros hx. change hx with (pr1 hx,,pr2 hx). generalize (pr1 hx), (pr2 hx). clear hx. intros x1 x2 ; simpl pr1 ; simpl pr2 ; clear x ; intros ->. apply NR_to_hr_le ; simpl. rewrite !isrunit_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.
imports: UniMath.Algebra.Groups UniMath.Foundations.Preamble UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals