proposition: Lemma max_prefix_max_snoc l1 l2 k1 k2 k3 x1 x2 : max_prefix l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
proof: Proof. intros Hl ->. destruct (prefix_snoc_not k3 x2). eapply max_prefix_max_alt; eauto. - rewrite (max_prefix_fst_alt _ _ _ _ _ Hl). apply prefix_app, prefix_cons, prefix_nil. - rewrite (max_prefix_snd_alt _ _ _ _ _ Hl). apply prefix_app, prefix_cons, prefix_nil. Qed.
imports: stdpp(options)