proposition: Theorem ps_normal_mul_comm : ∀ ps₁ ps₂, normalise_ps (ps₁ * ps₂)%ps ≐ normalise_ps (ps₂ * ps₁)%ps.
proof: Proof. intros ps₁ ps₂. unfold normalise_ps; simpl. remember (series_stretch (cm_factor ps₁ ps₂) (ps_terms ps₁)) as s₁ eqn:Hs₁ . remember (series_stretch (cm_factor ps₂ ps₁) (ps_terms ps₂)) as s₂ eqn:Hs₂ . rewrite series_mul_comm. remember (series_order (s₂ * s₁)%ser 0) as n eqn:Hn . destruct n as [n| ]; [ idtac | reflexivity ]. constructor; simpl. unfold gcd_ps; simpl. rewrite series_mul_comm. f_equal; [ f_equal; apply Z.add_comm | f_equal ]. f_equal; [ f_equal; apply Z.add_comm | idtac ]. unfold cm; rewrite Pos.mul_comm; reflexivity. unfold cm; rewrite Pos.mul_comm, series_mul_comm. unfold gcd_ps; simpl. do 3 f_equal. f_equal; [ f_equal; apply Z.add_comm | idtac ]. unfold cm; rewrite Pos.mul_comm; reflexivity. unfold gcd_ps; simpl. unfold cm; rewrite Pos.mul_comm, series_mul_comm. remember (ps_ordnum ps₁ * Zpos (ps_polydo ps₂))%Z as x eqn:Hx . remember (ps_ordnum ps₂ * Zpos (ps_polydo ps₁))%Z as y eqn:Hy . replace (x + y)%Z with (y + x)%Z by apply Z.add_comm. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat