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

op dvdz_ge1 (x n : int) : bool =
  1 <= x /\ x %| n.

(* smt can solve this, but as a learning exercise, we'll prove it
   by hand *)

lemma div_le (x n : int) :
  1 <= n => dvdz_ge1 x n => x <= n.
proof.
rewrite /dvdz_ge1 => ge1_n [ge1_x x_dvdz_n].
have eq_n : n = n %/ x * x by rewrite eq_sym -dvdz_eq.
rewrite eq_n -{1}div1r ler_pmul // (lez_trans 1) //.
case (1 <= n %/ x) => [// |].
rewrite -ltzNge ltz1 => le0_n_div_x.
have eq0_n_div_x : n %/ x = 0.
  apply lez_anti.
  split => [// | _].
  by rewrite divz_ge0 1:ltzE // (lez_trans 1).
have eq0_n : n = 0 by rewrite eq_n eq0_n_div_x.
have // : 1 <= 0 by rewrite -eq0_n.
qed.