Let x, g and m be given.

Assume Hm.

Let n be given.

Assume Hn Hmn.

Apply nat_Subq_add_ex m Hm n Hn Hmn to the current goal.

Let k be given.

Assume H.

Apply H to the current goal.

Assume Hk: nat_p k.

rewrite the current goal using add_nat_com k Hk m Hm (from left to right).

Assume H1: n = add_nat m k.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is SNo_sqrtaux_mon_lem x g m Hm k Hk.

∎