Lemma hr_to_NRneg_minus : ∏ x y : hr_commring, hr_to_NRneg x - hr_to_NRneg y <= hr_to_NRneg (x - y)%ring. 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.
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.