mod_nat: THEORY
%-----------------------------------------------------------------------
%
% NOTE: Given that "mod" is now defined in the prelude, this "mod" has
%       been renamed "nmod" 
%
%-----------------------------------------------------------------------
BEGIN
 
  n,k,n1,n2,c: VAR nat
  m,mk: VAR posnat
  i: VAR int

  IMPORTING div_nat

  nmod(n,m): below(m) = n - m*div(n,m)

  nmod_even    : LEMMA integer_pred(n/m) IMPLIES nmod(n,m) = 0

  nmod_lt_nat  : LEMMA n < m IMPLIES nmod(n,m) = n

  nmod_sum     : LEMMA n+i*m >= 0 IMPLIES nmod(n+i*m,m) = nmod(n,m)

  nmod_sum_nat : LEMMA n1 < m AND n2 < m IMPLIES
                          nmod(n1+n2,m) = IF n1 + n2 < m THEN n1+n2
                                         ELSE n1 + n2 - m
                                         ENDIF

  nmod_it_is   : LEMMA n = k + m*c AND k < m IMPLIES k = nmod(n,m)

  nmod_zero    : LEMMA nmod(0,m) = 0

  nmod_one     : LEMMA nmod(1,m) = IF m = 1 THEN 0
                                  ELSE 1
                                  ENDIF

  nmod_of_nmod  : LEMMA nmod(n + nmod(k,m), m) = nmod(n+k, m)

  nmod_mult    : LEMMA nmod(nmod(n,mk*m),m) = nmod(n,m)

END mod_nat