proposition: Lemma split_list_app_cons : forall (A : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) t l, In t l -> let (l1, l2) := split_list eqA l t in l = l1 ++ t :: l2.
proof: Proof. induction l as [ | a l ]. contradiction. simpl; elim (eqA t a); intro eq_t_a. intros _; subst; trivial. intros [eq_t_a' | In_t]. absurd (t = a); auto. generalize (IHl In_t); destruct (split_list eqA l t); intro; subst; auto. Defined.
imports: List Arith