let i, m be Nat; :: thesis: ( i <= m & m <= i + 1 & not i = m implies i = m -' 1 )
assume that
A1: i <= m and
A2: m <= i + 1 and
A3: i <> m ; :: thesis: i = m -' 1
i < m by A1, A3, XXREAL_0:1;
then i + 1 <= m by NAT_1:13;
then m = i + 1 by A2, XXREAL_0:1;
hence i = m -' 1 by NAT_D:34; :: thesis: verum