proposition: Lemma NonnegativeRationals_to_NonnegativeReals_plus : ∏ x y : NonnegativeRationals, NonnegativeRationals_to_NonnegativeReals (x + y)%NRat = NonnegativeRationals_to_NonnegativeReals x + NonnegativeRationals_to_NonnegativeReals y.
proof: Proof. intros x y. apply Dcuts_eq_is_eq. intros r. split. - intros Hr. generalize (eq0orgt0NonnegativeRationals y) ; apply sumofmaps ; intros Hy. 2: generalize (eq0orgt0NonnegativeRationals x) ; apply sumofmaps ; intros Hx. + rewrite Hy in Hr |- * ; clear y Hy. rewrite isrunit_zeroNonnegativeRationals in Hr. rewrite isrunit_Dcuts_plus_zero. exact Hr. + rewrite Hx in Hr |- * ; clear x Hx. rewrite islunit_zeroNonnegativeRationals in Hr. rewrite islunit_Dcuts_plus_zero. exact Hr. + assert (Hxy : (0 < x + y)%NRat). { apply ispositive_plusNonnegativeRationals_r. exact Hy. } apply hinhpr ; right. exists ((r * (x / (x + y)))%NRat,,(r * (y / (x + y)))%NRat). simpl. split ; [ | split]. * unfold divNonnegativeRationals. rewrite <- isldistr_mult_plusNonnegativeRationals, <- isrdistr_mult_plusNonnegativeRationals, isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals. { reflexivity. } exact Hxy. * unfold divNonnegativeRationals. rewrite <- isassoc_multNonnegativeRationals, (iscomm_multNonnegativeRationals _ x), isassoc_multNonnegativeRationals. pattern x at 3 ; rewrite <- (isrunit_oneNonnegativeRationals x). apply multNonnegativeRationals_ltcompat_l. { exact Hx. } rewrite <- (isrinv_NonnegativeRationals (x + y)%NRat). ** apply multNonnegativeRationals_ltcompat_r. *** apply ispositive_invNonnegativeRationals. exact Hxy. *** exact Hr. ** exact Hxy. * unfold divNonnegativeRationals. rewrite <- isassoc_multNonnegativeRationals, (iscomm_multNonnegativeRationals _ y), isassoc_multNonnegativeRationals. pattern y at 3 ; rewrite <- (isrunit_oneNonnegativeRationals y). apply multNonnegativeRationals_ltcompat_l. { exact Hy. } rewrite <- (isrinv_NonnegativeRationals (x + y)%NRat). ** apply multNonnegativeRationals_ltcompat_r. *** apply ispositive_invNonnegativeRationals. exact Hxy. *** exact Hr. ** exact Hxy. - apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Hrx | intros Hry] | intros xy ; rewrite (pr1 (pr2 xy))] ; simpl. + eapply istrans_lt_le_ltNonnegativeRationals, plusNonnegativeRationals_le_r. exact Hrx. + eapply istrans_lt_le_ltNonnegativeRationals, plusNonnegativeRationals_le_l. exact Hry. + apply plusNonnegativeRationals_ltcompat. * exact (pr1 (pr2 (pr2 xy))). * exact (pr2 (pr2 (pr2 xy))). 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