proposition: Theorem ps_normal_add_assoc : ∀ ps₁ ps₂ ps₃, normalise_ps ((ps₁ + ps₂) + ps₃)%ps ≐ normalise_ps (ps₁ + (ps₂ + ps₃))%ps.
proof: Proof. intros ps₁ ps₂ ps₃. unfold normalise_ps; simpl. rewrite ps_terms_add_assoc. remember (ps₂ + ps₃)%ps as x. remember (series_order (ps_terms_add ps₁ x) 0) as n. subst x. rename Heqn into Hn. symmetry in Hn. destruct n as [n| ]; [ constructor; simpl | reflexivity ]. rewrite ps_terms_add_assoc. rewrite gcd_ps_add_assoc. do 2 f_equal. unfold ps_ordnum_add; simpl. unfold ps_ordnum_add; simpl. unfold cm_factor, cm; simpl. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Z.min_assoc. do 2 rewrite Pos2Z.inj_mul. do 2 rewrite Z.mul_assoc. f_equal; [ idtac | rewrite Z.mul_shuffle0; reflexivity ]. f_equal; rewrite Z.mul_shuffle0; reflexivity. rewrite ps_terms_add_assoc. rewrite gcd_ps_add_assoc. unfold cm_factor, cm; simpl; unfold cm; simpl. do 4 rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. reflexivity. rewrite ps_terms_add_assoc. rewrite gcd_ps_add_assoc. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series