proposition: Lemma app_eq_cons x y z (a : A): x ++ y = a :: z -> (x = nil /\ y = a :: z) \/ exists x', x = a :: x' /\ z = x' ++ y.
proof: Proof. intro H. destruct x as [|b x]. - now left. - right. injection H as ->. now exists x. Qed.
imports: PeanoNat