floor_div_lems: THEORY
BEGIN

  i,k: VAR int
  j: VAR nonzero_integer
  x: VAR real

%-------------------- following now in prelude --------------------
%
%  floor_val:   LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k 
%
%  floor_small: LEMMA  abs(i) < abs(j) IMPLIES
%                         floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF
%
%  floor_eq_0:  LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1


  n: VAR nat
  m: VAR posnat

  floor_small_nat: LEMMA n < m IMPLIES floor(n/m) = 0

  is_multiple: LEMMA integer_pred(i/j) = (EXISTS k: i = k*j)
 
END floor_div_lems