proposition: Lemma NonnegativeRationals_to_NonnegativeReals_mult : ∏ x y : NonnegativeRationals, NonnegativeRationals_to_NonnegativeReals (x * y)%NRat = NonnegativeRationals_to_NonnegativeReals x * NonnegativeRationals_to_NonnegativeReals y.
proof: 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.
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