proposition: Lemma equiv_rem_add : forall (a:A) (P Q:set), (P a) -> equiv Q (rem a P) -> equiv (add a Q) P.
proof: Proof. intros; assert (incl Q (rem a P)); auto. assert (incl (rem a P) Q); auto. case (incl_rem_add_iff a P Q); auto. Qed.
imports: Coq(Arith) Coq(Lt)