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;