proposition: Theorem series_stretch_mul : ∀ a b k, (series_stretch k (a * b) = series_stretch k a * series_stretch k b)%ser.
proof: Proof. intros a b k. constructor; intros i; simpl. destruct (zerop (i mod Pos.to_nat k)) as [H₂| H₂]. apply Nat.mod_divides in H₂; auto with Arith. destruct H₂ as (c, Hc). rewrite Hc. rewrite Nat.mul_comm. rewrite Nat.div_mul; auto with Arith. unfold convol_mul; simpl. rename k into n, i into k. symmetry. apply inserted_0_summation; auto with Arith. intros i Hi. destruct (zerop (i mod Pos.to_nat n)) as [| H₂]; [ contradiction | idtac ]. rewrite rng_mul_0_l; reflexivity. intros i. rewrite Nat.mul_comm. rewrite <- Nat.mul_sub_distr_r. rewrite Nat.mod_mul; auto with Arith; simpl. rewrite Nat.mod_mul; auto with Arith; simpl. rewrite Nat.div_mul; auto with Arith; simpl. rewrite Nat.div_mul; auto with Arith; simpl. unfold convol_mul. symmetry. apply all_0_summation_0; intros j Hj. destruct (zerop (j mod Pos.to_nat k)) as [H₄| H₄]. destruct (zerop ((i - j) mod Pos.to_nat k)) as [H₅| H₅]. apply Nat.mod_divides in H₄; auto with Arith. apply Nat.mod_divides in H₅; auto with Arith. destruct H₄ as (c, Hc). destruct H₅ as (d, Hd). subst j. apply Nat.add_sub_eq_nz in Hd. subst i. rewrite <- Nat.mul_add_distr_l in H₂; auto with Arith. rewrite Nat.mul_comm in H₂. rewrite Nat.mod_mul in H₂; auto with Arith. exfalso; revert H₂; apply Nat.lt_irrefl. intros H. rewrite H in Hd. apply Nat.sub_0_le in Hd. destruct Hj as (_, Hj). apply Nat.le_antisymm in Hd; auto with Arith. rewrite <- Hd in H₂. rewrite Nat.mul_comm in H₂. rewrite Nat.mod_mul in H₂; auto with Arith. exfalso; revert H₂; apply Nat.lt_irrefl. rewrite rng_mul_comm. rewrite shifted_in_stretched; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. rewrite shifted_in_stretched; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat