Let n be given.

Assume Hn.

Assume H1.

Apply H1 to the current goal.

Let f be given.

Assume Hf: inj (ordsucc n) n f.

Apply Hf to the current goal.

Assume Hf1 Hf2.

An exact proof term for the current goal is PigeonHole_nat n Hn f Hf1 Hf2.

∎