proposition: Lemma max_prefix_fst_alt l1 l2 k1 k2 k3 : max_prefix l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
proof: Proof. intros. pose proof (max_prefix_fst l1 l2). by destruct (max_prefix l1 l2) as [[]?]; simplify_eq. Qed.
imports: stdpp(options)