proposition: Lemma max_suffix_max_snoc l1 l2 k1 k2 k3 x1 x2 : max_suffix l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
proof: Proof. intros Hl ->. destruct (suffix_cons_not x2 k3). eapply max_suffix_max_alt; eauto. - rewrite (max_suffix_fst_alt _ _ _ _ _ Hl). by apply (suffix_app [x2]), suffix_app_r. - rewrite (max_suffix_snd_alt _ _ _ _ _ Hl). by apply (suffix_app [x2]), suffix_app_r. Qed.
imports: stdpp(options)