Lemma Dcuts_NQmult_mult : ∏ (x : NonnegativeRationals) (y : Dcuts) (Hx0 : (0 < x)%NRat), Dcuts_NQmult x y Hx0 = Dcuts_mult (NonnegativeRationals_to_Dcuts x) y. Proof. intros x y Hx0. apply Dcuts_eq_is_eq. intros r ; split. - apply hinhuniv. intros ry. generalize (is_Dcuts_open _ _ (pr2 (pr2 ry))). apply hinhfun ; intros ry'. exists (((x * (pr1 ry)) / (pr1 ry'))%NRat,, (pr1 ry')). simpl. assert (Hry' : (0 < pr1 ry')%NRat). { eapply istrans_le_lt_ltNonnegativeRationals, (pr2 (pr2 ry')). apply isnonnegative_NonnegativeRationals. } split ; [ | split]. + unfold divNonnegativeRationals. rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals. * exact (pr1 (pr2 ry)). * exact Hry'. + pattern x at 2. rewrite <- (isrunit_oneNonnegativeRationals x). unfold divNonnegativeRationals. rewrite isassoc_multNonnegativeRationals. apply multNonnegativeRationals_ltcompat_l. * exact Hx0. * rewrite <- (isrinv_NonnegativeRationals (pr1 ry')). ** apply multNonnegativeRationals_ltcompat_r. *** apply ispositive_invNonnegativeRationals. exact Hry'. *** exact (pr2 (pr2 ry')). ** exact Hry'. + exact (pr1 (pr2 ry')). - apply hinhfun ; simpl. intros xy. exists (pr1 (pr1 xy) * pr2 (pr1 xy) / x). split. + rewrite iscomm_multNonnegativeRationals. unfold divNonnegativeRationals. rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals. * exact (pr1 (pr2 xy)). * exact Hx0. + apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 xy))). pattern (pr2 (pr1 xy)) at 2. rewrite <- (isrunit_oneNonnegativeRationals (pr2 (pr1 xy))), <- (isrinv_NonnegativeRationals x), <- isassoc_multNonnegativeRationals. * apply multNonnegativeRationals_lecompat_r. rewrite iscomm_multNonnegativeRationals. apply multNonnegativeRationals_lecompat_l. apply lt_leNonnegativeRationals. exact (pr1 (pr2 (pr2 xy))). * exact Hx0. 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.