(* 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.