proposition: Lemma size_finite_rem: forall (P:set) (a:A) (f:finite P), (P a) -> size f = S (size (finite_rem a f)).
proof: Proof. induction f; intros. case (equiv_empty_false a e H). simpl; case (decA x a); simpl; intros. case e0; unfold eq_rect_r;simpl; auto. rewrite size_equiv; auto. rewrite IHf; auto. case (e a); unfold add; intuition. case n0; auto. Qed.
imports: Coq(Arith) Coq(Lt)