proposition: Lemma Dcuts_mult_lt_l : ∏ x x' y : Dcuts, Dcuts_mult x y < Dcuts_mult x' y -> x < x'.
proof: Proof. intros x x' y. apply hinhuniv ; intros r. generalize (pr2 (pr2 r)). apply hinhfun ; intros xy. exists (pr1 (pr1 xy)) ; split. - intro H ; apply (pr1 (pr2 r)). apply hinhpr ; exists (pr1 xy). repeat split. + exact (pr1 (pr2 xy)). + exact H. + exact (pr2 (pr2 (pr2 xy))). - exact (pr1 (pr2 (pr2 xy))). 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