Lemma Dcuts_NQmult_bot : Dcuts_def_bot Dcuts_NQmult_val. Proof. intros r Hr n Hn. revert Hr ; apply hinhfun ; intros ry. generalize (isdeceq_NonnegativeRationals r 0%NRat) ; apply sumofmaps ; intros Hr0. - rewrite Hr0 in Hn. apply NonnegativeRationals_eq0_le0 in Hn. exists 0%NRat. rewrite Hn ; simpl. split. + now rewrite israbsorb_zero_multNonnegativeRationals. + apply Y_bot with (1 := pr2 (pr2 ry)). apply isnonnegative_NonnegativeRationals. - set (ny := pr1 ry * (n / r)%NRat). exists ny. split. + unfold ny ; simpl. rewrite <- isassoc_multNonnegativeRationals, <- (pr1 (pr2 ry)). rewrite multdivNonnegativeRationals. * reflexivity. * now apply NonnegativeRationals_neq0_gt0. + apply Y_bot with (1 := pr2 (pr2 ry)). apply multNonnegativeRationals_le1_r. now apply divNonnegativeRationals_le1. 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.