proposition: Lemma isassoc_Dcuts_mult : isassoc Dcuts_mult.
proof: Proof. intros x y z. apply Dcuts_eq_is_eq ; intro r ; split. - apply hinhuniv ; intros xyz. generalize (pr1 (pr2 (pr2 xyz))). apply hinhfun ; intros xy. pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 xy)), isassoc_multNonnegativeRationals. exists (pr1 (pr1 xy),,(pr2 (pr1 xy) * pr2 (pr1 xyz))) ; simpl ; repeat split. + exact (pr1 (pr2 (pr2 xy))). + apply hinhpr ; exists (pr2 (pr1 xy),,pr2 (pr1 (xyz))). repeat split. * exact (pr2 (pr2 (pr2 xy))). * exact (pr2 (pr2 (pr2 xyz))). - apply hinhuniv ; intros xyz. generalize (pr2 (pr2 (pr2 xyz))). apply hinhfun ; intros yz. pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 yz)), <- isassoc_multNonnegativeRationals. exists ((pr1 (pr1 xyz) * pr1 (pr1 yz)) ,, pr2 (pr1 yz)) ; simpl ; repeat split. + apply hinhpr ; 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