proposition: Theorem ps_polydo_adjust_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃, ps_polydo (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps) = ps_polydo (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)).
proof: Proof. intros ps₁ ps₂ ps₃; simpl. unfold cm; simpl. unfold cm_factor. rewrite Pos.mul_1_r. do 2 rewrite Pos.mul_assoc. rewrite Pos_mul_shuffle0. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat