proposition: Lemma incl_add_rem : forall (a:A) (P Q:set), ~ Q a -> incl (add a Q) P -> incl Q (rem a P) .
proof: Proof. unfold rem, add, incl; intros; auto. case (decA x a); intros; auto. subst; case H; auto. Qed.
imports: Coq(Arith) Coq(Lt)