proposition: Theorem nth_skipn_eq : forall (A : Set)(y x: nat)(ls : list A)(def : A), nth x (skipn y ls) def = nth (x + y) ls def.
proof: Proof. induction y; intuition; simpl in *. rewrite Nat.add_0_r. trivial. destruct ls. rewrite nth_nil. rewrite nth_nil. trivial. rewrite Nat.add_comm. simpl. rewrite Nat.add_comm. eapply IHy. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation