divides_lems: THEORY
%----------------------------------------------------------------------------
% 
%  Divisibility
%
%  Author: Rick Butler
%
%  NOTE.  This theory joins the old divisibility theory with the prelude
%         definitions.  If you hate the fact that the prelude definition of divides
%         using x as an integer, you can use divides_rew instead.
%
%----------------------------------------------------------------------------
BEGIN


   n,n1,n2: VAR nat
   m,m1,m2: VAR posnat
   i,j,k,ip,jp: VAR int
   nn,mm,ii,jj,kk: VAR nzint

   divides_rew: LEMMA divides(mm,i) = (EXISTS (k: int): i = mm*k)

   divides_lt: LEMMA i /= 0 IMPLIES divides(mm,i) IMPLIES mm <= abs(i)

   divides_lt_abs: LEMMA divides(mm,ii) IMPLIES abs(mm) <= abs(ii)

   divides_mod: LEMMA divides(m,i) = (mod(i,m) = 0)

   divides_sym: LEMMA divides(mm,ii) = divides(mm,-ii)

   divides_plus : LEMMA divides(mm,i) AND divides(mm,j) IMPLIES divides(mm,i+j)


   divides_plus_1: LEMMA mm > 1 IMPLIES 
                           divides(mm,ii) IMPLIES NOT divides(mm,ii+1)

   IMPORTING min_posnat

   lcm(m1,m2): int = min({k: posnat | divides(m1,k) AND divides(m2,k)})

   IMPORTING max_bounded_posnat

   gcd_noem: LEMMA nonempty?({k: posnat | divides(k, i) AND divides(k, j)})

   gcd_prep: LEMMA  
      FORALL (i: int, j: {jj: int | i = 0 => jj /= 0}):
        EXISTS (UB: posnat):
        FORALL (y: ({k: posnat | divides(k, i) AND divides(k, j)})):
          y <= UB
 

END divides_lems