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;