proposition: Lemma max_suffix_max_alt l1 l2 k1 k2 k3 k : max_suffix l1 l2 = (k1, k2, k3) → k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
proof: Proof. intro. pose proof (max_suffix_max l1 l2 k). by destruct (max_suffix l1 l2) as [[]?]; simplify_eq. Qed.
imports: stdpp(options)