proposition: Lemma Dcuts_NQmult_finite : Dcuts_def_finite Dcuts_NQmult_val.
proof: Proof. revert Y_finite. apply hinhfun. intros y. exists (x * pr1 y). unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros ry. generalize (pr1 (pr2 ry)). apply gtNonnegativeRationals_noteq. apply (pr2 (lt_gtNonnegativeRationals _ _)). apply (multNonnegativeRationals_ltcompat_l x (pr1 ry) (pr1 y) Hx). apply notge_ltNonnegativeRationals. intro Hy' ; apply (pr2 y). apply Y_bot with (pr1 ry). - exact (pr2 (pr2 ry)). - exact Hy'. 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