proposition: Theorem lap_convol_mul_1_l : ∀ cl i len, length cl = (i + len)%nat → lap_eq (lap_convol_mul r [1%K] cl i len) (List.skipn i cl).
proof: Proof. intros cl i len Hlen. revert cl i Hlen. induction len; intros. simpl. rewrite Nat.add_0_r in Hlen. rewrite list_skipn_overflow; subst; reflexivity. simpl. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite rng_mul_1_l, Nat.sub_0_r. rewrite all_0_summation_0. rewrite Nat.add_succ_r, <- Nat.add_succ_l in Hlen. rewrite rng_add_0_r, IHlen; [ clear | assumption ]. apply lap_eq_skipn_succ. intros j (Hj, Hji). destruct j; [ exfalso; revert Hj; apply Nat.nle_succ_0 | idtac ]. destruct j; rewrite rng_mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation