proposition: Lemma remove_remove_comm : forall l x y, remove x (remove y l) = remove y (remove x l).
proof: Proof. intro l; induction l as [| z l IHl]; simpl; intros x y. - reflexivity. - destruct (eq_dec y z); simpl; destruct (eq_dec x z); try rewrite IHl; auto. + subst; symmetry; apply remove_cons. + simpl; destruct (eq_dec y z); tauto. Qed.
imports: PeanoNat