proposition: Lemma isassoc_Dcuts_plus : isassoc Dcuts_plus.
proof: Proof. intros x y z. apply Dcuts_eq_is_eq ; intro r ; split. - apply hinhuniv, sumofmaps ; simpl pr1. + apply sumofmaps. * apply hinhuniv, sumofmaps. { apply sumofmaps ; intros Hr. - now apply hinhpr ; left ; left. - apply hinhpr ; left ; right. now apply hinhpr ; left ; left. } { intros xy. apply hinhpr ; right ; exists (pr1 xy). repeat split. - exact (pr1 (pr2 xy)). - exact (pr1 (pr2 (pr2 xy))). - apply hinhpr ; left ; left. exact (pr2 (pr2 (pr2 xy))). } * intros Hr. apply hinhpr ; left ; right. now apply hinhpr ; left ; right. + intros xyz. generalize (pr1 (pr2 (pr2 xyz))) ; apply hinhuniv, sumofmaps. * apply sumofmaps ; intros Hxy. { apply hinhpr ; right ; exists (pr1 xyz). repeat split. - exact (pr1 (pr2 xyz)). - exact Hxy. - apply hinhpr ; left ; right. exact (pr2 (pr2 (pr2 xyz))). } { apply hinhpr ; left ; right. apply hinhpr ; right ; exists (pr1 xyz). repeat split. - exact (pr1 (pr2 xyz)). - exact Hxy. - exact (pr2 (pr2 (pr2 xyz))). } * intros xy. apply hinhpr ; right ; exists (pr1 (pr1 xy),,pr2 (pr1 xy) + pr2 (pr1 xyz)). repeat split ; simpl. { pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 xy)). now apply isassoc_plusNonnegativeRationals. } { exact (pr1 (pr2 (pr2 xy))). } { apply hinhpr ; right ; exists (pr2 (pr1 xy),,pr2 (pr1 xyz)). repeat split. - exact (pr2 (pr2 (pr2 xy))). - exact (pr2 (pr2 (pr2 xyz))). } - apply hinhuniv, sumofmaps. + apply sumofmaps. * intros Hr. apply hinhpr ; left ; left. now apply hinhpr ; left ; left. * apply hinhuniv, sumofmaps. { apply sumofmaps ; intros Hr. - apply hinhpr ; left ; left. now apply hinhpr ; left ; right. - now apply hinhpr ; left ; right. } { intros yz ; simpl in * |-. apply hinhpr ; right ; exists (pr1 yz). repeat split. - exact (pr1 (pr2 yz)). - apply hinhpr ; left ; right. exact (pr1 (pr2 (pr2 yz))). - exact (pr2 (pr2 (pr2 yz))). } + intros xyz. generalize (pr2 (pr2 (pr2 xyz))) ; apply hinhuniv, sumofmaps. * apply sumofmaps ; intros Hyz. { apply hinhpr ; left ; left. apply hinhpr ; right ; exists (pr1 xyz). repeat split. - exact (pr1 (pr2 xyz)). - exact (pr1 (pr2 (pr2 xyz))). - exact Hyz. } { apply hinhpr ; right ; exists (pr1 xyz). repeat split. - exact (pr1 (pr2 xyz)). - apply hinhpr ; left ; left. exact (pr1 (pr2 (pr2 xyz))). - exact Hyz. } * intros yz. apply hinhpr ; right ; exists ((pr1 (pr1 xyz)+ pr1 (pr1 yz),, pr2 (pr1 yz))). repeat split ; simpl. { pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 yz)). now rewrite isassoc_plusNonnegativeRationals. } { apply hinhpr ; right ; exists (pr1 (pr1 xyz),,(pr1 (pr1 yz))). repeat split. - exact (pr1 (pr2 (pr2 xyz))). - exact (pr1 (pr2 (pr2 yz))). } { exact (pr2 (pr2 (pr2 yz))). } 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