proposition: Lemma combine_firstn : forall (l : list A) (l' : list B) (n : nat), firstn n (combine l l') = combine (firstn n l) (firstn n l').
proof: Proof. intro l; induction l as [| x l IHl]; intros l' n. - simpl. repeat (rewrite firstn_nil). reflexivity. - destruct l' as [| x' l']. + simpl. repeat (rewrite firstn_nil). rewrite combine_nil. reflexivity. + simpl. destruct n as [| n]; [reflexivity|]. repeat (rewrite firstn_cons). simpl. rewrite IHl. reflexivity. Qed.
imports: PeanoNat