proposition: Theorem normalise_ps_mul_adjust_l : ∀ ps₁ ps₂ n k, normalise_ps (ps_mul ps₁ ps₂) ≐ normalise_ps (ps_mul (adjust_ps n k ps₁) ps₂).
proof: Proof. intros ps₁ ps₂ n k. remember (Pos.to_nat (ps_polydo ps₂) * n)%nat as m eqn:Hm . rewrite ps_normal_adjust_eq with (n := m) (k := k); subst m. unfold ps_mul; simpl. unfold adjust_ps; simpl. unfold cm, cm_factor; simpl. rewrite Pos2Z.inj_mul, Z.mul_assoc. rewrite Z.mul_sub_distr_r. rewrite Z.mul_shuffle0. rewrite <- Z.add_sub_swap. rewrite <- Z.mul_add_distr_r. rewrite Nat.mul_comm. rewrite Nat2Z.inj_mul. rewrite positive_nat_Z. rewrite Pos_mul_shuffle0. rewrite series_stretch_mul. rewrite stretch_shift_series_distr. do 3 rewrite <- series_stretch_stretch. rewrite series_shift_mul. rewrite Pos.mul_comm. rewrite series_mul_comm, Pos.mul_comm, series_mul_comm. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat