proposition: Theorem ps_ordnum_adjust_normalise_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃ ps₄ ps₅ n, ps₄ = adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps → ps₅ = adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps) → series_order (ps_terms ps₄) 0 = fin n → series_order (ps_terms ps₅) 0 = fin n → ps_ordnum (normalise_ps ps₄) = ps_ordnum (normalise_ps ps₅).
proof: Proof. intros ps₁ ps₂ ps₃ ps₄ ps₅ n Hps₄ Hps₅ Hn₄ Hn₅. erewrite ps_ordnum_normalise; try reflexivity; try eassumption. erewrite ps_ordnum_normalise; try reflexivity; try eassumption. rewrite Hps₄, Hps₅. rewrite ps_ordnum_adjust_mul_add₂_distr_l. rewrite ps_polydo_adjust_mul_add₂_distr_l. rewrite ps_terms_adjust_mul_add₂_distr_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat