let n, k be Nat; :: thesis: ( n < k implies n <= k - 1 )
assume n < k ; :: thesis: n <= k - 1
then n + 1 <= k by NAT_1:13;
then (n + 1) - 1 <= k - 1 by XREAL_1:9;
hence n <= k - 1 ; :: thesis: verum