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

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