proposition: Theorem list_nth_add : ∀ k la lb, (List.nth k (lap_add la lb) 0 = List.nth k la 0 + List.nth k lb 0)%K.
proof: Proof. intros k la lb. revert la lb. induction k; intros. destruct la as [| a]; simpl; [ rewrite rng_add_0_l; reflexivity | idtac ]. destruct lb as [| b]; simpl; [ rewrite rng_add_0_r; reflexivity | idtac ]. reflexivity. destruct la as [| a]; simpl; [ rewrite rng_add_0_l; reflexivity | idtac ]. destruct lb as [| b]; simpl; [ rewrite rng_add_0_r; reflexivity | idtac ]. apply IHk. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation