proposition: Lemma size_inter_add_notin : forall P Q R (decP:dec P)(x:A)(nq:~Q x)(FQ:finite Q)(e:equiv R (add x Q)), ~ P x -> size (finite_inter decP (fin_eq_add nq FQ e))=size (finite_inter decP FQ).
proof: Proof. intros; simpl. case (decP x); intro; try contradiction. rewrite size_equiv; trivial. Qed.
imports: Coq(Arith) Coq(Lt)