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