proposition: Lemma Qmult_uncurry_assoc : forall (i j k:Q) (b : Qpos), Qabs i <= `b -> Qabs j <= `b -> Qabs k <= `b -> Qabs (j*k) <= `b -> Qabs (i*j) <= `b -> Qmult_uncurry b (Qmult_uncurry b (i, j), k) == Qmult_uncurry b (i, Qmult_uncurry b (j,k)).
proof: Proof. intros. simpl. apply Qabs_Qle_condition in H. destruct H as [ilower iupper]. apply Qabs_Qle_condition in H0. destruct H0 as [jlower jupper]. apply Qabs_Qle_condition in H1. destruct H1 as [klower kupper]. apply Qabs_Qle_condition in H2. destruct H2 as [jklower jkupper]. apply Qabs_Qle_condition in H3. destruct H3 as [ijlower ijupper]. assert (forall a:Q, a <= `b -> Qmin (`b) a == a)%Q as elim_min. { apply Qle_min_r. } assert (forall a:Q, -(`b) <= a -> Qmax (-(`b)) a == a)%Q as elim_max. { intros. apply Qle_max_r, H. } rewrite (elim_min j jupper). rewrite (elim_min i iupper). rewrite (elim_min k kupper). rewrite (elim_max j jlower). rewrite (elim_max i ilower). rewrite (elim_max k klower). rewrite (elim_min (j*k) jkupper). rewrite (elim_min (i*j) ijupper). rewrite (elim_max (j*k) jklower). rewrite (elim_max (i*j) ijlower). rewrite Qmult_assoc. reflexivity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names