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;