Lemma Dcuts_plus_bot : Dcuts_def_bot Dcuts_plus_val. Proof. intros r Hr n Hn. revert Hr ; apply hinhfun ; apply sumofmaps ; [apply sumofmaps ; intros Hr | intros xy]. - left ; left. now apply X_bot with r. - left ; right. now apply Y_bot with r. - right. 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 isrunit_zeroNonnegativeRationals. * 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) * (n / r))%NRat). set (ny := (pr2 (pr1 xy) * (n / r))%NRat). exists (nx,,ny). repeat split. * unfold nx,ny ; simpl. rewrite <- isrdistr_mult_plusNonnegativeRationals, <- (pr1 (pr2 xy)). rewrite multdivNonnegativeRationals. ** reflexivity. ** now apply NonnegativeRationals_neq0_gt0. * apply X_bot with (1 := pr1 (pr2 (pr2 xy))). apply multNonnegativeRationals_le1_r. now apply divNonnegativeRationals_le1. * 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.