let
b
be
Nat
;
:: thesis:
b
!
<=
b
|^
b
per
cases
(
b
>=
2 or
b
=
0
or
b
=
1 )
by
NAT_1:23
;
suppose
b
>=
2 ;
:: thesis:
b
!
<=
b
|^
b
hence
b
!
<=
b
|^
b
by
Th24
;
:: thesis:
verum
end;
suppose
b
=
0
;
:: thesis:
b
!
<=
b
|^
b
hence
b
!
<=
b
|^
b
by
NEWTON:4
,
NEWTON:12
;
:: thesis:
verum
end;
suppose
b
=
1 ;
:: thesis:
b
!
<=
b
|^
b
hence
b
!
<=
b
|^
b
by
NEWTON:13
;
:: thesis:
verum
end;
end;