proposition: Lemma isldistr_Dcuts_max_plus : isldistr Dcuts_max Dcuts_plus.
proof: Proof. intros x y z. apply Dcuts_eq_is_eq. intros r ; split. - apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Zr | ] | intros zxy ; rewrite (pr1 (pr2 zxy)) ; generalize (pr2 (pr2 (pr2 zxy))) ]. + apply hinhpr. left. apply hinhpr. left. now left. + apply hinhfun. apply sumofmaps ; [intros Xr | intros Yr]. * left. apply hinhpr. left. now right. * right. apply hinhpr. left. now right. + apply hinhfun. apply sumofmaps ; [intros Xr | intros Yr]. * left. apply hinhpr. right. exists (pr1 zxy). repeat split. ** exact (pr1 (pr2 (pr2 zxy))). ** exact Xr. * right. apply hinhpr. right. exists (pr1 zxy). repeat split. ** exact (pr1 (pr2 (pr2 zxy))). ** exact Yr. - apply hinhuniv ; apply sumofmaps ; apply hinhuniv ; apply sumofmaps. + apply sumofmaps ; [ intros Zr | intros Xr] ; apply hinhpr ; left. * now left. * right. apply hinhpr. now left. + intros zx ; rewrite (pr1 (pr2 zx)). apply hinhpr. right. exists (pr1 zx). repeat split. * exact (pr1 (pr2 (pr2 zx))). * apply hinhpr. left. exact (pr2 (pr2 (pr2 zx))). + apply sumofmaps ; [intros Zr | intros Yr] ; apply hinhpr ; left. * now left. * right. apply hinhpr. now right. + intros zx ; rewrite (pr1 (pr2 zx)). apply hinhpr. right. exists (pr1 zx). repeat split. * exact (pr1 (pr2 (pr2 zx))). * apply hinhpr. right. exact (pr2 (pr2 (pr2 zx))). 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