(* Exercise coq_list_02 *)

(* Those are the definitions from the previous exercise: *)

Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

Fixpoint append (l m : natlist) {struct l} : natlist :=
  match l with
  | nil => m
  | cons x xs => cons x (append xs m)
  end.
  
(* Now let us prove that the append operation is associative *)

Lemma append_assoc : forall l m n,
  append (append l m) n = append l (append m n).

Proof.
intros l m n.
induction l.
- simpl. auto.
- simpl. rewrite IHl. reflexivity.
Qed.