Let x be given.

Assume Hx.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

An exact proof term for the current goal is exp_SNo_nat_mul_add x Hx m (omega_nat_p m Hm) n (omega_nat_p n Hn).

∎