proposition: Lemma combine_firstn_r : forall (l : list A) (l' : list B), combine l l' = combine (firstn (length l') l) l'.
proof: Proof. intros l l'. generalize dependent l. induction l' as [| x' l' IHl']; intros l. - simpl. apply combine_nil. - destruct l as [| x l]; [reflexivity|]. simpl. specialize IHl' with l. rewrite <- IHl'. reflexivity. Qed.
imports: PeanoNat