proposition: Lemma Add_split a l l' : Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2.
proof: Proof. induction 1 as [l|x ? ? ? IHAdd]. - exists nil; exists l; split; trivial. - destruct IHAdd as (l1 & l2 & Hl & Hl'). exists (x::l1); exists l2; split; simpl; f_equal; trivial. Qed.
imports: PeanoNat