assume let
aŽb it
& ,
by expanding
and such
arbitrary in
, and
. and
should want_to
inner middle
conclude know
a any
natural ‚
= is
on to
this which
-- ndiff
int_entire the
= are_equal_to
0 zero
positive_integer ‚
integer z
as be
-- monus
applying by
n natural
integers …
if suppose
arbitrary z
integers z
case if
case otherwise
expanding unfolding
by unfolding
is_not ¨
: either
prove show
analysis split
contracts contradicts
z …
: that
.aŽ­ Ž­
(a+-b+-c;0) (a+-b+-c;imax(0+-c;0)
: be
assumptions supposition
follow follows
n ‚
assume suppose
. then
integers n
need_to should
assumption fact
else otherwise
0Ž.aŽªa 0ŽŽªa
our the
if otherwise
simplify y
are be
integers numbers
cases choices
arbitrary integers
need_to want_to
, .
let suppose
and or
‚¶ …·¸ ·¸ ‚ positive_integer 
monus ndiff
use using
by from
given let
conclusion result