2つの自然数列を結合したものの要素数が夫々の自然数列の要素数の和に等しいことの証明

Inductive nat_list : Set :=

NNil : nat_list

NCons : nat -> nat_list -> nat_list.

Fixpoint nlength (ls : nat_list) : nat :=
match ls with

NNil => O

NCons _ ls' => S (nlength ls')

end.

Fixpoint napp (ls1 ls2 : nat_list) : nat_list :=
match ls1 with

NNil => ls2

NCons n ls1' => NCons n (napp ls1' ls2 )

end.

Theorem nlength_napp : forall ls1 ls2 : nat_list, nlength (napp ls1 ls2 ) = plus (nlength ls1 ) (nlength ls2 ).
induction ls1.
simpl. reflexivity.
simpl. intros ls2. rewrite IHls1. reflexivity.
Qed.