Details About PVS Ints Library

  
     div,             % integer division
     rem,             % old version of "rem", prelude version supercedes
     mod_div_lems,    % modular arithmetic lemmas that involve div
     mod_lems,        % modular arithmetic lemmas
     gcd,             % greatest common divisior
     tdiv, tmod,      % versions that trunc away from zero for neg arg
     max_upto,        % max of a set of upto
     max_below,       % max of a set of below
     div_nat,         % integer division over nats
     mod_nat,         % mod over nats
     abstract_min,    % defines min over type T satisfying P
     abstract_max,    % defines max over type T satisfying P
     floor_div_lems,
     floor_more,
     infinite_primes,      % set of primes has infinite cardinality
     max_below,
     max_bounded_posnat,
     min_posnat,
     nat_fun_props,
     primes,               % definition of prime numbers
     prime_factorization,  % factorization into primes
     unique_factorization, % factorization is unique