Lemma Dcuts_minus_eq_zero: ∏ x y : Dcuts, x <= y -> Dcuts_minus x y = 0. Proof. intros X Y Hxy. apply Dcuts_eq_is_eq ; intros r ; split. - apply hinhuniv ; intros x. apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 x)). rewrite islunit_zeroNonnegativeRationals. apply (pr2 (pr2 x)). left ; simple refine (Hxy _ _). exact (pr1 (pr2 x)). - intro H. now apply fromempty ; apply (Dcuts_zero_empty r). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.