proposition: Lemma hr_ex_inv : ∏ x : hr_commring, hr_ap_rel x 0%ring -> multinvpair hr_commring x.
proof: 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.
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