let m be Nat; :: thesis: for n being Integer holds
not not n mod (m + 1) = 0 & ... & not n mod (m + 1) = m
let n be Integer; :: thesis: not not n mod (m + 1) = 0 & ... & not n mod (m + 1) = m
reconsider i = n mod (m + 1) as Element of NAT by INT_1:3, INT_1:57;
take i ; :: thesis: ( 0 <= i & i <= m & n mod (m + 1) = i )
thus 0 <= i ; :: thesis: ( i <= m & n mod (m + 1) = i )
i < m + 1 by INT_1:58;
hence i <= m by NAT_1:13; :: thesis: n mod (m + 1) = i
thus n mod (m + 1) = i ; :: thesis: verum