let
c
be
Nat
;
:: thesis:
for
b
being
positive
Nat
holds
b
divides
(
b
+
c
)
!
let
b
be
positive
Nat
;
:: thesis:
b
divides
(
b
+
c
)
!
b
+
c
>=
b
+
0
by
XREAL_1:6
;
hence
b
divides
(
b
+
c
)
!
by
NEWTON:41
;
:: thesis:
verum