let
a
,
b
be
positive
Nat
;
:: thesis:
(
a
mod
b
=
b
mod
a
implies
a
=
b
)
per
cases
(
a
<
b
or
b
<
a
or
b
=
a
)
by
XXREAL_0:1
;
suppose
a
<
b
;
:: thesis:
(
a
mod
b
=
b
mod
a
implies
a
=
b
)
then
a
mod
b
=
a
by
NAT_D:24
;
hence
(
a
mod
b
=
b
mod
a
implies
a
=
b
)
by
NAT_D:1
;
:: thesis:
verum
end;
suppose
b
<
a
;
:: thesis:
(
a
mod
b
=
b
mod
a
implies
a
=
b
)
then
b
mod
a
=
b
by
NAT_D:24
;
hence
(
a
mod
b
=
b
mod
a
implies
a
=
b
)
by
NAT_D:1
;
:: thesis:
verum
end;
suppose
b
=
a
;
:: thesis:
(
a
mod
b
=
b
mod
a
implies
a
=
b
)
hence
(
a
mod
b
=
b
mod
a
implies
a
=
b
) ;
:: thesis:
verum
end;
end;