Let a, b and c be given.

Assume H.

Let p be given.

Assume Hp.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume Ha Hb Hc H.

Apply H to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume Hm.

Assume H.

Apply H to the current goal.

Let n be given.

Assume H.

Apply H to the current goal.

Assume Hn.

Assume H1: m * a + n * b = c.

An exact proof term for the current goal is Hp Ha Hb Hc m Hm n Hn H1.

∎