Let a, b and c be given.

Assume H.

Let p be given.

Assume Hp.

Apply int_lin_comb_E a b c H to the current goal.

Assume _ _ _.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn H1.

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

∎