proposition: Lemma minusNonnegativeRationals_plus_r : ∏ r q : NonnegativeRationals, r <= q -> (q - r) + r = q.
proof: 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.
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