proposition: Lemma infinite_diff_finite P Q (Q_dec : forall x, {Q x}+{~Q x}) : infinite P -> finite Q -> infinite (diff P Q).
proof: Proof. intros P_inf Q_fin P_Q_fin. apply P_inf. cut (finite (union P Q)). rewrite finite_union_eq. fo. rewrite <- union_diff, finite_union_eq; auto. Qed.
imports: Coq(Basics Morphisms Setoid Lia) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil SetUtil FinSet FunUtil BoundNat IotaUtil EpsilonUtil)