let k, m be Element of NAT ; :: thesis: ( k < m iff k <= m - 1 )

A1: now

assume k <= m - 1 ; :: thesis: k < m
then A2: k + 1 <= m by XREAL_1:21;
k < k + 1 by XREAL_1:31;
hence k < m by A2, XXREAL_0:2; :: thesis: verum

end;

now

assume k < m ; :: thesis: k <= m - 1
then k + 1 <= m by INT_1:20;
hence k <= m - 1 by XREAL_1:21; :: thesis: verum

end;

hence ( k < m iff k <= m - 1 ) by A1; :: thesis: verum