Lemma Dcuts_NQmult_finite : Dcuts_def_finite Dcuts_NQmult_val. 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.
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.