Lemma minusNonnegativeRationals_correct : ∏ (x y : NonnegativeRationals) (Hminus : y <= x), x - y = Rationals_to_NonnegativeRationals (pr1 x - pr1 y)%hq (hq0leminus _ _ Hminus). Proof. intros x y H. apply subtypePath_prop. unfold minusNonnegativeRationals, hnnq_minus. generalize (hqgthorleh (pr1 x) (pr1 y)). apply coprod_rect ; [intros Hgt | intros Hle]. - reflexivity. - generalize (isantisymmhqleh _ _ Hle H) ; intros Heq. rewrite coprod_rect_compute_2. generalize (hq0leminus (pr1 y) (pr1 x) H). rewrite Heq, hqrminus. intros H0. 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.