Lemma hr_ex_inv : ∏ x : hr_commring, hr_ap_rel x 0%ring -> multinvpair hr_commring x. Proof. intros x Hap. generalize (pr1 (hr_ap_lt _ _) Hap) ; apply sumofmaps ; intros Hlt ; simpl. - eexists ; split. + refine (hr_islinv_neg _ _). exact Hlt. + exact (hr_isrinv_neg _ _). - eexists ; split. + refine (hr_islinv_pos _ _). exact Hlt. + exact (hr_isrinv_pos _ _). Defined.
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.