proposition: Lemma minusNonnegativeRationals_plus_exchange : ∏ x y z : NonnegativeRationals, y <= x -> x - y + z = (x + z) - y.
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.RealNumbers.Sets UniMath.RealNumbers.Fields UniMath.Algebra.DivisionRig UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim