proposition: Lemma isaprop_Dcuts_ap_rel (X Y : Dcuts_set) : isaprop ((X < Y) ⨿ (Y < X)).
proof: Proof. apply (isapropcoprod (X < Y) (Y < X) (propproperty (X < Y)) (propproperty (Y < X)) (λ Hlt : X < Y, pr2 (Dcuts_le_ngt_rel Y X) (Dcuts_lt_le_rel X Y Hlt))). Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals