per cases ( 0 - n >= 0 or 0 - n < 0 ) ;
suppose 0 - n >= 0 ; :: thesis: 0 -' n = 0
then 0 - n = 0 ;
hence 0 -' n = 0 by XREAL_1:233; :: thesis: verum
end;
suppose 0 - n < 0 ; :: thesis: 0 -' n = 0
hence 0 -' n = 0 by XREAL_0:def 2; :: thesis: verum
end;
end;