proposition: Lemma isldistr_Dcuts_plus_mult : isldistr Dcuts_plus Dcuts_mult.
proof: Proof. intros x y z. apply Dcuts_eq_is_eq ; intro r ; split. - apply hinhuniv ; intros xyz. rewrite (pr1 (pr2 xyz)). generalize (pr2 (pr2 (pr2 xyz))). apply hinhfun ; apply sumofmaps ; [ apply sumofmaps ; [intros Xr | intros Yr] | intros xy ]. + left ; left ; apply hinhpr. exists (pr1 xyz) ; repeat split. * exact (pr1 (pr2 (pr2 xyz))). * exact Xr. + left ; right ; apply hinhpr. exists (pr1 xyz) ; repeat split. * exact (pr1 (pr2 (pr2 xyz))). * exact Yr. + rewrite (pr1 (pr2 xy)), isldistr_mult_plusNonnegativeRationals. right ; exists (pr1 (pr1 xyz) * pr1 (pr1 xy),, pr1 (pr1 xyz) * pr2 (pr1 xy)) ; repeat split. * apply hinhpr ; exists (pr1 (pr1 xyz),,pr1 (pr1 xy)). repeat split. ** exact (pr1 (pr2 (pr2 xyz))). ** exact (pr1 (pr2 (pr2 xy))). * apply hinhpr ; exists (pr1 (pr1 xyz),,pr2 (pr1 xy)). repeat split. ** exact (pr1 (pr2 (pr2 xyz))). ** exact (pr2 (pr2 (pr2 xy))). - apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps | intros zxzy ]. + apply hinhfun ; intros zx. rewrite (pr1 (pr2 zx)). exists (pr1 zx) ; repeat split. * exact (pr1 (pr2 (pr2 zx))). * apply hinhpr ; left ; left. exact (pr2 (pr2 (pr2 zx))). + apply hinhfun ; intros zy. rewrite (pr1 (pr2 zy)). exists (pr1 zy) ; repeat split. * exact (pr1 (pr2 (pr2 zy))). * apply hinhpr ; left ; right. exact (pr2 (pr2 (pr2 zy))). + rewrite (pr1 (pr2 zxzy)). generalize (pr1 (pr2 (pr2 zxzy))) (pr2 (pr2 (pr2 zxzy))). apply hinhfun2 ; intros zx zy. rewrite (pr1 (pr2 zx)), (pr1 (pr2 zy)). generalize (isdecrel_leNonnegativeRationals (NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy))) 0%NRat) ; apply sumofmaps ; [intros Heq| intros Hlt]. * apply NonnegativeRationals_eq0_le0 in Heq. apply NQmax_eq_zero in Heq. rewrite (pr1 Heq), (pr2 Heq). exists (0%NRat,,pr2 (pr1 zx)) ; simpl ; repeat split. ** rewrite !islabsorb_zero_multNonnegativeRationals. now apply isrunit_zeroNonnegativeRationals. ** apply (is_Dcuts_bot _ _ (pr1 (pr2 (pr2 zx)))). apply isnonnegative_NonnegativeRationals. ** apply hinhpr ; left ; left. exact (pr2 (pr2 (pr2 zx))). * apply notge_ltNonnegativeRationals in Hlt. exists (NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy)),, (pr1 (pr1 zx) * pr2 (pr1 zx) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy)) + (pr1 (pr1 zy) * pr2 (pr1 zy) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy))))) ; simpl ; repeat split. ** unfold divNonnegativeRationals. rewrite <- isrdistr_mult_plusNonnegativeRationals. now apply pathsinv0, multdivNonnegativeRationals. ** apply NQmax_case. *** exact (pr1 (pr2 (pr2 zx))). *** exact (pr1 (pr2 (pr2 zy))). ** apply hinhpr ; right. exists (pr1 (pr1 zx) * pr2 (pr1 zx) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy)) ,, pr1 (pr1 zy) * pr2 (pr1 zy) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy))) ; simpl ; repeat split. *** apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 zx))). rewrite iscomm_multNonnegativeRationals. unfold divNonnegativeRationals ; rewrite isassoc_multNonnegativeRationals. apply multNonnegativeRationals_le1_r, divNonnegativeRationals_le1. now apply NQmax_le_l. *** apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 zy))). rewrite iscomm_multNonnegativeRationals. unfold divNonnegativeRationals ; rewrite isassoc_multNonnegativeRationals. apply multNonnegativeRationals_le1_r, divNonnegativeRationals_le1. now apply NQmax_le_r. 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