let k, m be Element of NAT ; :: 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;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

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

hence
( k < m iff k <= m - 1 )
by A1; :: thesis: verumassume
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;then k + 1 <= m by INT_1:7;

hence k <= m - 1 by XREAL_1:19; :: thesis: verum