proposition: Theorem skipn_snd_split_app_cons : forall (A B : Type)(ls1 ls2 : list (A * B)) p, skipn (S (length ls1)) (snd (split (ls1 ++ (p :: ls2)))) = snd (split ls2).
proof: Proof. intuition idtac. assert (S (length ls1) = (length ls1 + 1))%nat. lia. rewrite H. rewrite <- skipn_sum. rewrite skipn_snd_split_app. simpl. destruct (split ls2); trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation