(* int-div-examp.ec *)

require import AllCore.

require import IntDiv StdOrder. (* lemmas for integer mod and div *)
import IntOrder.                (* lemmas about <, <= on int *)

(* n %/ x is the integer division of n by x, discarding any remainder

   n %% x is the remainder of integer division of n by x

   x %| n tests whether x divides n, i.e., n %% x = 0

   %/ and %% are actually abbreviations, defined in terms of edivz;
   consequently, when using `search` to look for lemmas involving
   these abbreviations, one must search for `edivz` instead. *)

lemma div_le (x n : int) :
  1 <= x => 1 <= n => x %| n => x <= n.
proof.

qed.