Let a, b and c be given.

Assume H.

Apply int_lin_comb_E a b c H to the current goal.

Assume _ _ Hc.

Let m be given.

Assume _.

Let n be given.

Assume _ _.

An exact proof term for the current goal is Hc.

∎