proposition: Theorem ps_monom_mul_l : ∀ c d n, (ps_monom (c * d)%K n = ps_monom c 0 * ps_monom d n)%ps.
proof: Proof. intros c d n. progress unfold ps_monom; simpl. apply mkps_morphism; simpl; [ idtac | idtac | reflexivity ]. constructor; intros i; simpl. destruct i; simpl. progress unfold convol_mul; simpl. rewrite summation_only_one; simpl. rewrite Nat.mod_0_l; auto with Arith; simpl. rewrite Nat.div_0_l; auto with Arith; simpl. progress unfold convol_mul; simpl. rewrite all_0_summation_0; [ reflexivity | idtac ]. intros j (_, Hj). rewrite divmod_div. rewrite fold_sub_succ_l. rewrite Nat.div_1_r. destruct (zerop (j mod Pos.to_nat (Qden n))) as [H₁| H₁]. apply Nat.mod_divides in H₁; auto with Arith. destruct H₁ as (e, He). rewrite Nat.mul_comm in He. rewrite He. rewrite Nat.div_mul; auto with Arith. destruct (zerop e) as [H₂| H₂]. subst e; rewrite Nat.sub_0_r; simpl. rewrite rng_mul_0_r; reflexivity. rewrite rng_mul_0_l; reflexivity. rewrite rng_mul_0_l; reflexivity. rewrite Z.mul_1_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat