proposition: Lemma hr_to_NRneg_minus : ∏ x y : hr_commring, hr_to_NRneg x - hr_to_NRneg y <= hr_to_NRneg (x - y)%ring.
proof: Proof. intros x y. rewrite hr_opp_minus. pattern x at 1 ; rewrite <- (grinvinv hr_commring x) ; pattern y at 1 ; rewrite <- (grinvinv hr_commring y). change (hr_to_NRneg (- (- x))%ring - hr_to_NRneg (- (- y))%ring <= hr_to_NRneg (- (- x - - y))%ring). rewrite !hr_to_NRneg_opp. apply hr_to_NRpos_minus. 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