Lemma hr_islinv_pos : ∏ (x : hr_commring) (Hap : hr_lt_rel 0%ring x), (NR_to_hr (invNonnegativeReals (hr_to_NRpos x) (pr1 (pr2 (hr_to_NR_positive _) Hap)) ,, 0%NR) * x)%ring = 1%ring. Proof. intros x Hap. pattern x at 3; rewrite <- (hr_to_NR_bij x). rewrite NR_to_hr_mult ; simpl. rewrite !islabsorb_zero_multNonnegativeReals , !isrunit_zero_plusNonnegativeReals. rewrite islinv_invNonnegativeReals. rewrite <- (hr_to_NR_bij 1%ring), hr_to_NR_one. apply maponpaths. apply maponpaths. erewrite <- israbsorb_zero_multNonnegativeReals. apply maponpaths. apply (pr2 (pr2 (hr_to_NR_positive x) Hap)). 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.