proposition: Lemma in_remove: forall l x y, In x (remove y l) -> In x l /\ x <> y.
proof: Proof. intro l; induction l as [|z l IHl]; intros x y Hin. - inversion Hin. - simpl in Hin. destruct (eq_dec y z) as [Heq|Hneq]; subst; split. + right; now apply IHl with z. + intros Heq; revert Hin; subst; apply remove_In. + inversion Hin; subst; [left; reflexivity|right]. now apply IHl with y. + destruct Hin as [Hin|Hin]; subst. * now intros Heq; apply Hneq. * intros Heq; revert Hin; subst; apply remove_In. Qed.
imports: PeanoNat