proposition: Lemma app_inv_tail: forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.
proof: Proof. intros l. induction l as [|a l IHl]. - intros ? ?. now rewrite !app_nil_r. - intros ? ?. change (a :: l) with ([a] ++ l). rewrite !app_assoc. now intros [? ?] %IHl %app_inj_tail_iff. Qed.
imports: PeanoNat