proposition: Theorem skipn_snd_split_app_cons_gen : forall (A B : Type)(ls1 ls2 : list (A * B)) p n, n = (S (length ls1)) -> skipn n (snd (split (ls1 ++ (p :: ls2)))) = snd (split ls2).
proof: Proof. intuition idtac. subst. apply skipn_snd_split_app_cons. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation