proposition: Theorem firstn_combine : forall (A B : Type)(lsA : list A)(lsB : list B) n, firstn n (combine lsA lsB) = combine (firstn n lsA) (firstn n lsB).
proof: Proof. induction lsA; intuition idtac; simpl in *. destruct n; trivial. destruct lsB; simpl in *. destruct n; trivial. destruct n; simpl in *; trivial. f_equal; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation