proposition: Theorem skipn_S_eq : forall (A : Set)(ls : list A) n a, nth_option ls n = Some a -> skipn n ls = a :: (skipn (S n) ls).
proof: Proof. induction ls; intuition; simpl in *. discriminate. destruct n; simpl in *. inversion H; clear H; subst. trivial. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation