proposition: Lemma max_suffix_snd_alt l1 l2 k1 k2 k3 : max_suffix l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
proof: Proof. intro. pose proof (max_suffix_snd l1 l2). by destruct (max_suffix l1 l2) as [[]?]; simplify_eq. Qed.
imports: stdpp(options)