Lemma Dcuts_mult_lt_l : ∏ x x' y : Dcuts, Dcuts_mult x y < Dcuts_mult x' y -> x < x'. 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.
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.