proposition: Lemma hr_to_NR_positive : ∏ x : hr_commring, (hr_to_NRpos x ≠ 0 × hr_to_NRneg x = 0) <-> hr_lt_rel 0%ring x.
proof: 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 _). generalize (pr1 (hr_to_NR x)), (pr2 (hr_to_NR x)) ; intros x1 x2 ; simpl pr1 ; simpl pr2 ; clear x ; intros H1 ; rewrite (pr2 H1). apply NR_to_hr_lt ; simpl. rewrite !isrunit_zero_plusNonnegativeReals. now apply ispositive_apNonnegativeReals, (pr1 H1). - 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. - apply_pr2 hr_to_NR_nonnegative. now apply hr_lt_le. 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