Lemma isldistr_Dcuts_max_plus : isldistr Dcuts_max Dcuts_plus. 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.
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.