proposition: Lemma finite_rem : forall (P:set) (a:A), finite P -> finite (rem a P).
proof: Proof. induction 1; intuition. apply fin_eq_empty. unfold rem,empty,equiv; intuition. apply (equiv_empty_false x e); auto. case (decA x a); intros. apply fin_equiv with Q; subst; auto. apply equiv_add_rem; auto. apply fin_eq_add with x (rem a Q); auto. subst; unfold rem; intuition. apply equiv_trans with (rem a (add x Q)); auto. Defined.
imports: Coq(Arith) Coq(Lt)