mod_nat: THEORY BEGIN n,k,n1,n2,c: VAR nat m,mk: VAR posnat i: VAR int IMPORTING div_nat mod(n,m): below(m) = n - m*div(n,m) mod_even : LEMMA integer_pred(n/m) IMPLIES mod(n,m) = 0 mod_lt_nat : LEMMA n < m IMPLIES mod(n,m) = n mod_sum : LEMMA n+i*m >= 0 IMPLIES mod(n+i*m,m) = mod(n,m) mod_sum_nat : LEMMA n1 < m AND n2 < m IMPLIES mod(n1+n2,m) = IF n1 + n2 < m THEN n1+n2 ELSE n1 + n2 - m ENDIF mod_it_is : LEMMA n = k + m*c AND k < m IMPLIES k = mod(n,m) mod_zero : LEMMA mod(0,m) = 0 mod_one : LEMMA mod(1,m) = IF m = 1 THEN 0 ELSE 1 ENDIF mod_of_mod : LEMMA mod(n + mod(k,m), m) = mod(n+k, m) mod_mult : LEMMA mod(mod(n,mk*m),m) = mod(n,m) END mod_nat