let
k
be non
zero
Nat
;
:: thesis:
(
k
-'
1
)
+
2
=
(
k
+
2
)
-'
1
k
>=
1
by
NAT_2:19
;
hence
(
k
-'
1)
+
2
=
(
k
+
2
)
-'
1
by
NAT_D:38
;
:: thesis:
verum