proposition: Lemma in_in_remove : forall l x y, x <> y -> In x l -> In x (remove y l).
proof: Proof. intro l; induction l as [|z l IHl]; simpl; intros x y Hneq Hin. - apply Hin. - destruct (eq_dec y z); subst. + destruct Hin. * exfalso; now apply Hneq. * now apply IHl. + simpl; destruct Hin; [now left|right]. now apply IHl. Qed.
imports: PeanoNat