let i be natural Number ; :: thesis: i -' 2 = (i -' 1) -' 1
per cases ( i >= 2 or i < 2 ) ;
suppose A1: i >= 2 ; :: thesis: i -' 2 = (i -' 1) -' 1
then 1 <= i by XXREAL_0:2;
then i - 1 >= 0 by XREAL_1:48;
then A2: i -' 1 = i - 1 by XREAL_0:def 2;
i - 1 >= (1 + 1) - 1 by A1, XREAL_1:9;
then (i - 1) - 1 >= 1 - 1 by XREAL_1:9;
then (i -' 1) -' 1 = i - 2 by A2, XREAL_0:def 2;
hence i -' 2 = (i -' 1) -' 1 by XREAL_0:def 2; :: thesis: verum
end;
suppose A3: i < 2 ; :: thesis: i -' 2 = (i -' 1) -' 1
then i - 2 < 2 - 2 by XREAL_1:9;
then A4: i -' 2 = 0 by XREAL_0:def 2;
A5: (i + 1) - 1 <= (1 + 1) - 1 by A3, NAT_1:13;
now :: thesis: ( ( 1 <= i & i -' 2 = (i -' 1) -' 1 ) or ( i < 1 & i -' 2 = (i -' 1) -' 1 ) )
per cases ( 1 <= i or i < 1 ) ;
case 1 <= i ; :: thesis: i -' 2 = (i -' 1) -' 1
then i = 1 by A5, XXREAL_0:1;
then (i -' 1) -' 1 = 0 -' 1 by XREAL_1:232;
hence i -' 2 = (i -' 1) -' 1 by A4, Th35; :: thesis: verum
end;
case i < 1 ; :: thesis: i -' 2 = (i -' 1) -' 1
then i - 1 < 1 - 1 by XREAL_1:9;
then (i -' 1) -' 1 = 0 -' 1 by XREAL_0:def 2;
hence i -' 2 = (i -' 1) -' 1 by A4, Th35; :: thesis: verum
end;
end;
end;
hence i -' 2 = (i -' 1) -' 1 ; :: thesis: verum
end;
end;