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