proposition: Lemma fin_add_in : forall (a:A) (P:set), finite P -> finite (add a P).
proof: Proof. intros a P FP; case (finite_dec FP a); intro. apply fin_equiv with P; auto. apply equiv_sym; auto. apply fin_add; auto. Defined.
imports: Coq(Arith) Coq(Lt)