Let m be given.
Let n be given.
We prove the intermediate
claim LmS:
SNo m.
An
exact proof term for the current goal is
int_SNo m Hm.
We prove the intermediate
claim LnS:
SNo n.
An
exact proof term for the current goal is
int_SNo n Hn.
We prove the intermediate
claim L2nS:
SNo (2 * n).
We prove the intermediate
claim L2mS:
SNo (2 * m).
We prove the intermediate
claim Lm2nS:
SNo (- 2 * n).
We prove the intermediate
claim L1:
2 * n + 2 * m + - 2 * n = 2 * n + 1.
rewrite the current goal using H1 (from right to left).
We prove the intermediate
claim L2:
2 * (m + - n) = 1.
rewrite the current goal using L2 (from right to left) at position 2.
An
exact proof term for the current goal is
nat_2.
∎