Lemma hr_to_NR_negative : ∏ x : hr_commring, (hr_to_NRpos x = 0 × hr_to_NRneg x ≠ 0) <-> hr_lt_rel x 0%ring. Proof. intros x. repeat split. - pattern x at 3. rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero. unfold hr_to_NRpos, hr_to_NRneg. change (hr_to_NR x) with (pr1 (hr_to_NR x),,pr2 _). simpl pr1 ; simpl pr2 ; intros H2 ; rewrite (pr1 H2). apply NR_to_hr_lt ; simpl. rewrite !islunit_zero_plusNonnegativeReals. now apply ispositive_apNonnegativeReals, (pr2 H2). - apply_pr2 hr_to_NR_nonpositive. now apply hr_lt_le. - rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero in X. apply_pr2_in NR_to_hr_lt X. rewrite isrunit_zero_plusNonnegativeReals, islunit_zero_plusNonnegativeReals in X. apply_pr2 ispositive_apNonnegativeReals. eapply istrans_le_lt_ltNonnegativeReals, X. now apply isnonnegative_NonnegativeReals. 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.