We prove the intermediate
claim L1:
x = 0.
An exact proof term for the current goal is Hxnp.
An exact proof term for the current goal is H1.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using
mul_SNo_zeroL y Hy (from left to right).
∎