let k, m be Integer; :: thesis: ( k < m iff k <= m - 1 )

A1: now :: thesis: ( k <= m - 1 implies k < m )

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

end;

now :: thesis: ( k < m implies k <= m - 1 )

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

end;

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