let
a
be
Nat
;
:: thesis:
a
mod
1
=
0
a
=
(
1
*
a
)
+
0
;
hence
a
mod
1
=
0
by
NAT_D:def 2
;
:: thesis:
verum