proposition: Theorem series_shift_mul : ∀ a b n, (series_shift n (a * b)%ser = series_shift n a * b)%ser.
proof: Proof. intros a b n. constructor; intros k; simpl. destruct (lt_dec k n) as [H₂| H₂]. symmetry; unfold convol_mul; simpl. apply all_0_summation_0; intros i Hi. destruct (lt_dec i n) as [H₁| H₁]. rewrite rng_mul_0_l; reflexivity. exfalso; apply H₁. eapply le_lt_trans; [ idtac | eassumption ]. destruct Hi; assumption. apply Nat.nlt_ge in H₂. unfold convol_mul. symmetry. destruct n. rewrite Nat.sub_0_r. apply summation_compat; intros i Hi. rewrite series_shift_0; reflexivity. assert (k = (n + (k - n))%nat) as H by fast_omega H₂. rewrite H in |- * at 1. rewrite summation_ub_add. rewrite rng_add_comm. rewrite <- H. rewrite rng_add_comm. rewrite all_0_summation_0. rewrite rng_add_0_l. symmetry. rewrite summation_add_add_sub with (n := S n). rewrite Nat.add_0_l, Nat.sub_add; [ idtac | assumption ]. apply summation_compat; intros i Hi. assert (i = i - S n + S n)%nat as H₁ by fast_omega Hi. rewrite H₁ in |- * at 3. rewrite series_nth_add_shift. rewrite <- Nat.sub_add_distr. rewrite Nat.add_comm. rewrite <- H₁; reflexivity. intros i Hi; simpl. destruct (lt_dec i (S n)) as [H₁| H₁]. rewrite rng_mul_0_l; reflexivity. exfalso; apply H₁. apply Nat.lt_succ_r. destruct Hi; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat