proposition: Lemma foot_split_length: forall A (L : list A), match foot_split L with | (L', None) => length L' = length L | (L', Some _) => 1 + length L' = length L end.
proof: Proof. intros. generalize (foot_split_spec _ L). destruct (foot_split L). destruct o; intros; subst; auto. rewrite app_length. simpl. lia. destruct H. congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset