let i, j be Nat; :: thesis: ( i >= j implies j -' i = 0 )
assume A1: i >= j ; :: thesis: j -' i = 0

per cases ( i = j or i > j ) by A1, XXREAL_0:1;

suppose i = j ; :: thesis: j -' i = 0

hence j -' i = 0 by XREAL_1:232; :: thesis: verum

end;

suppose i > j ; :: thesis: j -' i = 0

then j - i < 0 by XREAL_1:49;
hence j -' i = 0 by XREAL_0:def 2; :: thesis: verum

end;

end;