We prove the intermediate
claim L2:
x = 0.
rewrite the current goal using
minus_SNo_0 (from right to left).
We will
prove - - x ≤ - 0.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H1.
rewrite the current goal using L2 (from left to right).
Use f_equal.
An
exact proof term for the current goal is
minus_SNo_0.