proposition: Theorem skipn_length : forall (A : Type)(ls : list A) n, length (skipn n ls) = length ls - n.
proof: Proof. induction ls; destruct n; intuition idtac; simpl in *; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation