proposition: Theorem skipn_combine : forall (A B : Type)(lsA : list A)(lsB : list B) n, skipn n (combine lsA lsB) = combine (skipn n lsA) (skipn n lsB).
proof: Proof. induction lsA; intuition idtac; simpl in *. repeat rewrite skipn_nil. trivial. destruct lsB; simpl in *. repeat rewrite skipn_nil. rewrite combine_nil_r. trivial. destruct n; simpl in *; trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation