proposition: Lemma Dcuts_NQmult_bot : Dcuts_def_bot Dcuts_NQmult_val.
proof: 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.
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