proposition: Lemma in_split_not_in_first: forall {A} (eq_dec: forall x y : A, {x = y} + {x <> y}) (x: A) (l: list A), In x l -> exists l1 l2, l = l1 ++ x :: l2 /\ ~ In x l1.
proof: Proof. intros ? ? ?. induction l; intros. - inversion H. - simpl in H. destruct (eq_dec a x). + exists nil, l. rewrite app_nil_l. subst a. split; auto. + destruct H. 1: exfalso; auto. specialize (IHl H). destruct IHl as [l1 [l2 [? ?]]]. exists (a :: l1), l2. simpl. rewrite H0. split; auto. intro. destruct H2; auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver