proposition: Theorem lap_eq_skipn_succ : ∀ cl i, lap_eq [List.nth i cl 0%K … List.skipn (S i) cl] (List.skipn i cl).
proof: Proof. intros cl i. revert i. induction cl as [| c]; intros; simpl. destruct i; constructor; reflexivity. destruct i; [ reflexivity | apply IHcl ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation