Let X and F be given.

Assume HinfX: infinite X.

Assume HfinF: finite F.

We will prove infinite (X ∖ F).

Assume HfinXF: finite (X ∖ F).

We prove the intermediate claim HfinU: finite ((X ∖ F) ∪ F).

An exact proof term for the current goal is (binunion_finite (X ∖ F) HfinXF F HfinF).

We prove the intermediate claim HXsubU: X ⊆ (X ∖ F) ∪ F.

Let x be given.

Assume HxX: x ∈ X.

Apply (xm (x ∈ F)) to the current goal.

Assume HxF: x ∈ F.

An exact proof term for the current goal is (binunionI2 (X ∖ F) F x HxF).

Assume HxnotF: ¬ (x ∈ F).

We prove the intermediate claim HxXF: x ∈ X ∖ F.

An exact proof term for the current goal is (setminusI X F x HxX HxnotF).

An exact proof term for the current goal is (binunionI1 (X ∖ F) F x HxXF).

We prove the intermediate claim HfinX: finite X.

An exact proof term for the current goal is (Subq_finite ((X ∖ F) ∪ F) HfinU X HXsubU).

An exact proof term for the current goal is (HinfX HfinX).

∎