Lemma minusNonnegativeRationals_plus_exchange : ∏ x y z : NonnegativeRationals, y <= x -> x - y + z = (x + z) - y. Proof. intros x y z Hxy. assert (Hxzy : y <= x + z). { apply istrans_leNonnegativeRationals with x. { exact Hxy. } apply plusNonnegativeRationals_le_r. } rewrite (minusNonnegativeRationals_correct _ _ Hxy), (minusNonnegativeRationals_correct _ _ Hxzy). revert Hxy Hxzy. intros. apply subtypePath_prop. change (pr1 x - pr1 y + pr1 z = (pr1 x + pr1 z) - pr1 y)%hq. now unfold hqminus ; rewrite !hqplusassoc, (hqpluscomm (pr1 z)). Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.