divisibility: THEORY BEGIN IMPORTING mod_nt 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(mm,i): bool = (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) % IMPORTING floor_div_props --- now in prelude 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 divisibility