proposition: Theorem skipn_app_gen : forall (A : Type)(n : nat)(ls1 ls2 : list A), skipn n (ls1 ++ ls2) = skipn n ls1 ++ (skipn (n - length ls1) ls2).
proof: Proof. induction n; destruct ls1; intuition idtac; simpl in *. apply IHn. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation