proposition: Lemma foot_split_spec: forall A (L : list A), match foot_split L with | (L', None) => L = L' /\ L' = nil | (L', Some a) => L = L' ++ a :: nil end.
proof: Proof. induction L; simpl. auto. destruct L. reflexivity. remember (foot_split (a0 :: L)). destruct p. destruct o. rewrite IHL. rewrite app_comm_cons. trivial. destruct IHL. congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset