proposition: Lemma minusNonnegativeRationals_correct : ∏ (x y : NonnegativeRationals) (Hminus : y <= x), x - y = Rationals_to_NonnegativeRationals (pr1 x - pr1 y)%hq (hq0leminus _ _ Hminus).
proof: 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.
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