Lemma plusNonnegativeRationals_minus_r : ∏ q r : NonnegativeRationals, (r + q) - q = r. Proof. intros q r. change r with (pr1 r,,pr2 r). generalize (pr1 r) (pr2 r) (pr1 q) (pr2 q) ; intros r' Hr q' Hq. rewrite (minusNonnegativeRationals_correct _ _ (plusNonnegativeRationals_le_l _ _)). apply subtypePath_prop. simpl pr1. unfold hqminus. rewrite hqplusassoc. rewrite (hqpluscomm (pr1 q)). rewrite hqlminus. rewrite hqplusr0. reflexivity. 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.