proposition: 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: 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.
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