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