Lemma minusNonnegativeRationals_plus_r : ∏ r q : NonnegativeRationals, r <= q -> (q - r) + r = q. Proof. intros r q H. unfold minusNonnegativeRationals, hnnq_minus. generalize (hqgthorleh (pr1 q) (pr1 r)). apply coprod_rect ; intros H'. - rewrite coprod_rect_compute_1. apply subtypePath_prop. unfold hqminus. pattern r at 4. simpl. generalize (pr1 r) (pr1 q) (pr2 r) (hq0leminus (pr1 r) (pr1 q) (hqlthtoleh (pr1 r) (pr1 q) H')) ; intros r' q' Hr Hrq. now rewrite hqplusassoc, hqlminus, hqplusr0. - rewrite coprod_rect_compute_2. apply subtypePath_prop. generalize (isantisymmhqleh _ _ H H'). simpl. generalize (pr1 r) (pr2 r) (pr1 q) ; intros r' Hr' q' Heq. now rewrite hqplusl0. 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.