proposition: Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B), In (x,y) (combine l l') -> In y l'.
proof: Proof. intro l; induction l as [|? ? IHl]. - simpl; intros; contradiction. - intro l'; destruct l'; simpl; auto; intros x y H. destruct H as [H|H]. + injection H; auto. + right; apply IHl with x; auto. Qed.
imports: PeanoNat