proposition: Theorem skipn_snd_split_app : forall (A B : Type)(ls1 ls2 : list (A * B)), skipn (length ls1) (snd (split (ls1 ++ ls2))) = snd (split ls2).
proof: Proof. induction ls1; intuition idtac; subst; simpl in *; trivial. remember (split (ls1 ++ ls2)) as z. destruct z. simpl in *. assert (l0 = (snd (split (ls1 ++ ls2)))). rewrite <- Heqz. trivial. rewrite H. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation