Lemma NonnegativeRationals_to_NonnegativeReals_mult : ∏ x y : NonnegativeRationals, NonnegativeRationals_to_NonnegativeReals (x * y)%NRat = NonnegativeRationals_to_NonnegativeReals x * NonnegativeRationals_to_NonnegativeReals y. Proof. intros x y. generalize (eq0orgt0NonnegativeRationals x) ; apply sumofmaps ; [intros -> | intros Hx]. - rewrite islabsorb_zero_multNonnegativeRationals, islabsorb_Dcuts_mult_zero. reflexivity. - rewrite <- (Dcuts_NQmult_mult _ _ Hx). apply Dcuts_eq_is_eq. intros r. split. + simpl ; intros Hr ; apply hinhpr. exists (r / x)%NRat. split. * apply pathsinv0, multdivNonnegativeRationals. exact Hx. * rewrite <- (isrunit_oneNonnegativeRationals y), <- (isrinv_NonnegativeRationals x), <- isassoc_multNonnegativeRationals. ** apply multNonnegativeRationals_ltcompat_r. *** apply ispositive_invNonnegativeRationals. exact Hx. *** rewrite iscomm_multNonnegativeRationals. exact Hr. ** exact Hx. + apply hinhuniv. simpl. intros ry. rewrite (pr1 (pr2 ry)). apply multNonnegativeRationals_ltcompat_l. * exact Hx. * exact (pr2 (pr2 ry)). 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.