Let a be given.

Assume Ha.

Let b be given.

Assume Hb.

Let c be given.

Assume Hc.

Assume H1.

We will prove a ∈ int ∧ b ∈ int ∧ c ∈ int ∧ ∃m n ∈ int, m * a + n * b = c.

Apply and4I to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is Hc.

An exact proof term for the current goal is H1.

∎