proposition: Theorem ps_mul_assoc : ∀ ps₁ ps₂ ps₃, (ps₁ * (ps₂ * ps₃) = (ps₁ * ps₂) * ps₃)%ps.
proof: Proof. intros ps₁ ps₂ ps₃. constructor. unfold normalise_ps; simpl. rewrite series_stretch_mul; symmetry. rewrite series_stretch_mul; symmetry. do 4 rewrite <- series_stretch_stretch. unfold cm, cm_factor; simpl. rewrite series_mul_assoc. remember (ps_polydo ps₂ * ps_polydo ps₃)%positive as c₂₃ eqn:Hc₂₃ . remember (ps_polydo ps₃ * ps_polydo ps₁)%positive as c₃₁ eqn:Hc₃₁ . remember (ps_polydo ps₁ * ps_polydo ps₂)%positive as c₁₂ eqn:Hc₁₂ . rewrite Pos.mul_comm in Hc₂₃; rewrite <- Hc₂₃. rewrite Pos.mul_comm in Hc₃₁; rewrite <- Hc₃₁. remember (series_stretch c₂₃ (ps_terms ps₁)) as s₁ eqn:Hs₁ . remember (series_stretch c₃₁ (ps_terms ps₂)) as s₂ eqn:Hs₂ . remember (series_stretch c₁₂ (ps_terms ps₃)) as s₃ eqn:Hs₃ . remember (series_mul (series_mul s₁ s₂) s₃) as s₁₂₃ eqn:Hs₁₂₃ . remember (series_order s₁₂₃ 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; [ idtac | reflexivity ]. unfold gcd_ps; simpl. progress unfold cm; simpl. progress unfold cm; simpl. do 2 rewrite Z.mul_add_distr_r. do 6 rewrite Pos2Z.inj_mul. do 3 rewrite Z.mul_assoc. do 2 rewrite Z.add_assoc. constructor; simpl. f_equal. f_equal. f_equal. f_equal. rewrite Hc₂₃, Pos2Z.inj_mul, Z.mul_assoc, Z.mul_shuffle0. reflexivity. rewrite Z.mul_shuffle0; reflexivity. rewrite Hc₁₂, Pos2Z.inj_mul, Z.mul_assoc, Z.mul_shuffle0. reflexivity. f_equal. do 2 f_equal. f_equal; [ f_equal | idtac ]; apply Z.mul_shuffle0. do 2 rewrite series_stretch_mul. do 4 rewrite <- series_stretch_stretch. rewrite <- Hc₁₂, <- Hc₂₃, <- Hc₃₁. rewrite Pos.mul_comm, <- Hc₃₁. rewrite <- Hs₁, <- Hs₂, <- Hs₃. rewrite series_mul_assoc; reflexivity. do 2 f_equal. f_equal. do 2 f_equal. f_equal; [ f_equal | idtac ]; apply Z.mul_shuffle0. do 2 rewrite series_stretch_mul. do 4 rewrite <- series_stretch_stretch. rewrite <- Hc₁₂, <- Hc₂₃, <- Hc₃₁. rewrite Pos.mul_comm, <- Hc₃₁. rewrite <- Hs₁, <- Hs₂, <- Hs₃. rewrite series_mul_assoc; reflexivity. constructor; intros i. do 4 rewrite series_stretch_mul at 1. do 8 rewrite <- series_stretch_stretch at 1. rewrite <- Hc₁₂, <- Hc₂₃, <- Hc₃₁. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, Pos.mul_comm, <- Hc₂₃. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, Pos.mul_comm, <- Hc₃₁. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, Pos.mul_comm, <- Hc₁₂. symmetry. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, <- Hc₃₁. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, <- Hc₁₂. rewrite series_mul_assoc. rewrite <- Hs₁, <- Hs₂, <- Hs₃. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat