proposition: Lemma exists_last : forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}.
proof: Proof. intro l; induction l as [|a l IHl]. - destruct 1; auto. - intros _. destruct l. + exists [], a; auto. + destruct IHl as [l' (a',H)]; try discriminate. rewrite H. exists (a::l'), a'; auto. Qed.
imports: PeanoNat