Theory List-Infinite.Util_Div

(*  Title:      Util_Div.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Results for division and modulo operators on integers›

theory Util_Div
imports Util_Nat
begin

subsection ‹Additional (in-)equalities with ‹div› and ‹mod››

corollary Suc_mod_le_divisor: "0 < m ⟹ Suc (n mod m) ≤ m"
by (rule Suc_leI, rule mod_less_divisor)

lemma mod_less_dividend: "⟦ 0 < m; m ≤ n ⟧ ⟹ n mod m < (n::nat)"
by (rule less_le_trans[OF mod_less_divisor])
(*lemma mod_le_dividend: "n mod m ≤ (n::nat)"*)
lemmas mod_le_dividend = mod_less_eq_dividend



lemma diff_mod_le: "(t - r) mod m ≤ (t::nat)"
by (rule le_trans[OF mod_le_dividend, OF diff_le_self])


(*corollary div_mult_cancel: "m div n * n = m - m mod (n::nat)"*)
lemmas div_mult_cancel = minus_mod_eq_div_mult [symmetric]

lemma mod_0_div_mult_cancel: "(n mod (m::nat) = 0) = (n div m * m = n)"
apply (insert eq_diff_left_iff[OF mod_le_dividend le0, of n m])
apply (simp add: mult.commute minus_mod_eq_mult_div [symmetric])
done

lemma div_mult_le: "(n::nat) div m * m ≤ n"
by (simp add: mult.commute minus_mod_eq_mult_div [symmetric])
lemma less_div_Suc_mult: "0 < (m::nat) ⟹ n < Suc (n div m) * m"
apply (simp add: mult.commute minus_mod_eq_mult_div [symmetric])
apply (rule less_add_diff)
by (rule mod_less_divisor)

lemma nat_ge2_conv: "((2::nat) ≤ n) = (n ≠ 0 ∧ n ≠ 1)"
by fastforce

lemma Suc0_mod: "m ≠ Suc 0 ⟹ Suc 0 mod m = Suc 0"
by (case_tac m, simp_all)
corollary Suc0_mod_subst: "
  ⟦ m ≠ Suc 0; P (Suc 0) ⟧ ⟹ P (Suc 0 mod m)"
by (blast intro: subst[OF Suc0_mod[symmetric]])
corollary Suc0_mod_cong: "
  m ≠ Suc 0 ⟹ f (Suc 0 mod m) = f (Suc 0)"
by (blast intro: arg_cong[OF Suc0_mod])


subsection ‹Additional results for addition and subtraction with ‹mod››

lemma mod_Suc_conv: "
  ((Suc a) mod m = (Suc b) mod m) = (a mod m = b mod m)"
by (simp add: mod_Suc)

lemma mod_Suc': "
  0 < n ⟹ Suc m mod n = (if m mod n < n - Suc 0 then Suc (m mod n) else 0)"
apply (simp add: mod_Suc)
apply (intro conjI impI)
 apply simp
apply (insert le_neq_trans[OF mod_less_divisor[THEN Suc_leI, of n m]], simp)
done

lemma mod_add:"
  ((a + k) mod m = (b + k) mod m) =
  ((a::nat) mod m = b mod m)"
by (induct "k", simp_all add: mod_Suc_conv)

corollary mod_sub_add: "
  k ≤ (a::nat) ⟹
  ((a - k) mod m = b mod m) = (a mod m = (b + k) mod m)"
by (simp add: mod_add[where m=m and a="a-k" and b=b and k=k, symmetric])


lemma mod_sub_eq_mod_0_conv: "
  a + b ≤ (n::nat) ⟹
  ((n - a) mod m = b mod m) = ((n - (a + b)) mod m = 0)"
by (insert mod_add[of "n-(a+b)" b m 0], simp)
lemma mod_sub_eq_mod_swap: "
  ⟦ a ≤ (n::nat); b ≤ n ⟧ ⟹
  ((n - a) mod m = b mod m) = ((n - b) mod m = a mod m)"
by (simp add: mod_sub_add add.commute)

lemma le_mod_greater_imp_div_less: "
  ⟦ a ≤ (b::nat); a mod m > b mod m ⟧ ⟹ a div m < b div m"
apply (rule ccontr, simp add: linorder_not_less)
apply (drule mult_le_mono1[of "b div m" _ m])
apply (drule add_less_le_mono[of "b mod m" "a mod m" "b div m * m" "a div m * m"])
apply simp_all
done

lemma less_mod_ge_imp_div_less: "⟦ a < (b::nat); a mod m ≥ b mod m ⟧ ⟹ a div m < b div m"
apply (case_tac "m = 0", simp)
apply (rule mult_less_cancel1[of m, THEN iffD1, THEN conjunct2])
apply (simp add: minus_mod_eq_mult_div [symmetric])
apply (rule order_less_le_trans[of _ "b - a mod m"])
apply (rule diff_less_mono)
apply simp+
done
corollary less_mod_0_imp_div_less: "⟦ a < (b::nat); b mod m = 0 ⟧ ⟹ a div m < b div m"
by (simp add: less_mod_ge_imp_div_less)

lemma mod_diff_right_eq: "
  (a::nat) ≤ b ⟹ (b - a) mod m = (b - a mod m) mod m"
proof -
  assume a_as:"a ≤ b"
  have "(b - a) mod m = (b - a + a div m * m) mod m" by simp
  also have "… = (b + a div m * m - a) mod m" using a_as by simp
  also have "… = (b + a div m * m - (a div m * m + a mod m)) mod m" by simp
  also have "… = (b + a div m * m - a div m * m - a mod m) mod m"
    by (simp only: diff_diff_left[symmetric])
  also have "… = (b - a mod m) mod m" by simp
  finally show ?thesis .
qed
corollary mod_eq_imp_diff_mod_eq: "
  ⟦ x mod m = y mod m; x ≤ (t::nat); y ≤ t ⟧ ⟹
  (t - x) mod m = (t - y) mod m"
by (simp only: mod_diff_right_eq)
lemma mod_eq_imp_diff_mod_eq2: "
  ⟦ x mod m = y mod m; (t::nat) ≤ x; t ≤ y ⟧ ⟹
  (x - t) mod m = (y - t) mod m"
apply (case_tac "m = 0", simp+)
apply (subst mod_mult_self2[of "x - t" m t, symmetric])
apply (subst mod_mult_self2[of "y - t" m t, symmetric])
apply (simp only: add_diff_assoc2 diff_add_assoc gr0_imp_self_le_mult2)
apply (simp only: mod_add)
done

lemma divisor_add_diff_mod_if: "
  (m + b mod m - a mod m) mod (m::nat)= (
  if a mod m ≤ b mod m
  then (b mod m - a mod m)
  else (m + b mod m - a mod m))"
apply (case_tac "m = 0", simp)
apply clarsimp
apply (subst diff_add_assoc, assumption)
apply (simp only: mod_add_self1)
apply (rule mod_less)
apply (simp add: less_imp_diff_less)
done
corollary divisor_add_diff_mod_eq1: "
  a mod m ≤ b mod m ⟹
  (m + b mod m - a mod m) mod (m::nat) = b mod m - a mod m"
by (simp add: divisor_add_diff_mod_if)
corollary divisor_add_diff_mod_eq2: "
  b mod m < a mod m ⟹
  (m + b mod m - a mod m) mod (m::nat) = m + b mod m - a mod m"
by (simp add: divisor_add_diff_mod_if)

lemma mod_add_mod_if: "
  (a mod m + b mod m) mod (m::nat)= (
  if a mod m + b mod m < m
  then a mod m + b mod m
  else a mod m + b mod m - m)"
apply (case_tac "m = 0", simp_all)
apply (clarsimp simp: linorder_not_less)
apply (simp add: mod_if[of "a mod m + b mod m"])
apply (rule mod_less)
apply (rule diff_less_conv[THEN iffD2], assumption)
apply (simp add: add_less_mono)
done
corollary mod_add_mod_eq1: "
  a mod m + b mod m < m ⟹
  (a mod m + b mod m) mod (m::nat) = a mod m + b mod m"
by (simp add: mod_add_mod_if)
corollary mod_add_mod_eq2: "
  m ≤ a mod m + b mod m⟹
  (a mod m + b mod m) mod (m::nat) = a mod m + b mod m - m"
by (simp add: mod_add_mod_if)

lemma mod_add1_eq_if: "
  (a + b) mod (m::nat) = (
  if (a mod m + b mod m < m) then a mod m + b mod m
  else a mod m + b mod m - m)"
by (simp add: mod_add_eq[symmetric, of a b] mod_add_mod_if)

lemma mod_add_eq_mod_conv: "0 < (m::nat) ⟹
  ((x + a) mod m = b mod m ) =
  (x mod m = (m + b mod m - a mod m) mod m)"
apply (simp only: mod_add_eq[symmetric, of x a])
apply (rule iffI)
 apply (drule sym)
 apply (simp add: mod_add_mod_if)
apply (simp add: mod_add_left_eq le_add_diff_inverse2[OF trans_le_add1[OF mod_le_divisor]])
done




lemma mod_diff1_eq: "
  (a::nat) ≤ b ⟹ (b - a) mod m = (m + b mod m - a mod m) mod m"
apply (case_tac "m = 0", simp)
apply simp
proof -
  assume a_as:"a ≤ b"
    and m_as: "0 < m"
  have a_mod_le_b_s: "a mod m ≤ b"
    by (rule le_trans[of _ a], simp only: mod_le_dividend, simp only: a_as)
  have "(b - a) mod m = (b - a mod m) mod m"
    using a_as by (simp only: mod_diff_right_eq)
  also have "… = (b - a mod m + m) mod m"
    by simp
  also have "… = (b + m - a mod m) mod m"
    using a_mod_le_b_s by simp
  also have "… = (b div m * m + b mod m + m - a mod m) mod m"
    by simp
  also have "… = (b div m * m + (b mod m + m - a mod m)) mod m"
    by (simp add: diff_add_assoc[OF mod_le_divisor, OF m_as])
  also have "… = ((b mod m + m - a mod m) + b div m * m) mod m"
    by simp
  also have "… = (b mod m + m - a mod m) mod m"
    by simp
  also have "… = (m + b mod m - a mod m) mod m"
    by (simp only: add.commute)
  finally show ?thesis .
qed
corollary mod_diff1_eq_if: "
  (a::nat) ≤ b ⟹ (b - a) mod m = (
    if a mod m ≤ b mod m then b mod m - a mod m
    else m + b mod m - a mod m)"
by (simp only: mod_diff1_eq divisor_add_diff_mod_if)
corollary mod_diff1_eq1: "
  ⟦ (a::nat) ≤ b; a mod m ≤ b mod m ⟧
  ⟹ (b - a) mod m = b mod m - a mod m"
by (simp add: mod_diff1_eq_if)
corollary mod_diff1_eq2: "
  ⟦ (a::nat) ≤ b; b mod m < a mod m⟧
  ⟹ (b - a) mod m = m + b mod m - a mod m"
by (simp add: mod_diff1_eq_if)


subsubsection ‹Divisor subtraction with ‹div› and ‹mod››

lemma mod_diff_self1: "
  0 < (n::nat) ⟹ (m - n) mod m = m - n"
by (case_tac "m = 0", simp_all)
lemma mod_diff_self2: "
  m ≤ (n::nat) ⟹ (n - m) mod m = n mod m"
by (simp add: mod_diff_right_eq)
lemma mod_diff_mult_self1: "
  k * m ≤ (n::nat) ⟹ (n - k * m) mod m = n mod m"
by (simp add: mod_diff_right_eq)
lemma mod_diff_mult_self2: "
  m * k ≤ (n::nat) ⟹ (n - m * k) mod m = n mod m"
by (simp only: mult.commute[of m k] mod_diff_mult_self1)

lemma div_diff_self1: "0 < (n::nat) ⟹ (m - n) div m = 0"
by (case_tac "m = 0", simp_all)
lemma div_diff_self2: "(n - m) div m = n div m - Suc 0"
apply (case_tac "m = 0", simp)
apply (case_tac "n < m", simp)
apply (case_tac "n = m", simp)
apply (simp add: div_if)
done

lemma div_diff_mult_self1: "
  (n - k * m) div m = n div m - (k::nat)"
apply (case_tac "m = 0", simp)
apply (case_tac "n < k * m")
 apply simp
 apply (drule div_le_mono[OF less_imp_le, of n _ m])
 apply simp
apply (simp add: linorder_not_less)
apply (rule iffD1[OF mult_cancel1_gr0[where k=m]], assumption)
apply (subst diff_mult_distrib2)
apply (simp only: minus_mod_eq_mult_div [symmetric])
apply (simp only: diff_commute[of _ "k*m"])
apply (simp only: mult.commute[of m])
apply (simp only: mod_diff_mult_self1)
done
lemma div_diff_mult_self2: "
  (n - m * k) div m = n div m - (k::nat)"
by (simp only: mult.commute div_diff_mult_self1)


subsubsection ‹Modulo equality and modulo of difference›

lemma mod_eq_imp_diff_mod_0:"
  (a::nat) mod m = b mod m ⟹ (b - a) mod m = 0"
  (is "?P ⟹ ?Q")
proof -
  assume as1: ?P
  have "b - a = b div m * m + b mod m - (a div m * m + a mod m)"
    by simp
  also have "… = b div m * m + b mod m - (a mod m + a div m * m)"
    by simp
  also have "… = b div m * m + b mod m - a mod m - a div m * m"
    by simp
  also have "… = b div m * m + b mod m - b mod m - a div m * m"
    using as1 by simp
  also have "… = b div m * m - a div m * m"
    by (simp only: diff_add_inverse2)
  also have "… = (b div m - a div m) * m"
    by (simp only: diff_mult_distrib)
  finally have "b - a = (b div m - a div m) * m" .
  hence "(b - a) mod m = (b div m - a div m) * m mod m"
    by (rule arg_cong)
  thus ?thesis by (simp only: mod_mult_self2_is_0)
qed
corollary mod_eq_imp_diff_dvd: "
  (a::nat) mod m = b mod m ⟹ m dvd b - a"
by (rule dvd_eq_mod_eq_0[THEN iffD2, OF mod_eq_imp_diff_mod_0])

lemma mod_neq_imp_diff_mod_neq0:"
  ⟦ (a::nat) mod m ≠ b mod m; a ≤ b ⟧ ⟹ 0 < (b - a) mod m"
apply (case_tac "m = 0", simp)
apply (drule le_imp_less_or_eq, erule disjE)
 prefer 2
 apply simp
apply (drule neq_iff[THEN iffD1], erule disjE)
 apply (simp add: mod_diff1_eq1)
apply (simp add: mod_diff1_eq2[OF less_imp_le] trans_less_add1[OF mod_less_divisor])
done
corollary mod_neq_imp_diff_not_dvd:"
  ⟦ (a::nat) mod m ≠ b mod m; a ≤ b ⟧ ⟹ ¬ m dvd b - a"
by (simp add: dvd_eq_mod_eq_0 mod_neq_imp_diff_mod_neq0)

lemma diff_mod_0_imp_mod_eq:"
  ⟦ (b - a) mod m = 0; a ≤ b ⟧ ⟹ (a::nat) mod m = b mod m"
apply (rule ccontr)
apply (drule mod_neq_imp_diff_mod_neq0)
apply simp_all
done
corollary diff_dvd_imp_mod_eq:"
  ⟦ m dvd b - a; a ≤ b ⟧ ⟹ (a::nat) mod m = b mod m"
by (rule dvd_eq_mod_eq_0[THEN iffD1, THEN diff_mod_0_imp_mod_eq])



lemma mod_eq_diff_mod_0_conv: "
  a ≤ (b::nat) ⟹ (a mod m = b mod m) = ((b - a) mod m = 0)"
apply (rule iffI)
apply (rule mod_eq_imp_diff_mod_0, assumption)
apply (rule diff_mod_0_imp_mod_eq, assumption+)
done
corollary mod_eq_diff_dvd_conv: "
  a ≤ (b::nat) ⟹ (a mod m = b mod m) = (m dvd b - a)"
by (rule dvd_eq_mod_eq_0[symmetric, THEN subst], rule mod_eq_diff_mod_0_conv)


subsection ‹Some additional lemmata about integer ‹div› and ‹mod››

lemma zmod_eq_imp_diff_mod_0:
  "a mod m = b mod m ⟹ (b - a) mod m = 0" for a b m :: int
  by (simp add: mod_diff_cong)
  
(*lemma int_mod_distrib: "int (n mod m) = int n mod int m"*)
lemmas int_mod_distrib = zmod_int

lemma zdiff_mod_0_imp_mod_eq__pos:"
  ⟦ (b - a) mod m = 0; 0 < (m::int) ⟧ ⟹ a mod m = b mod m"
  (is "⟦ ?P; ?Pm ⟧ ⟹ ?Q")
proof -
  assume as1: ?P
    and as2: "0 < m"

  obtain r1 where a_r1:"r1 = a mod m" by blast
  obtain r2 where b_r2:"r2 = b mod m" by blast

  obtain q1 where a_q1: "q1 = a div m" by blast
  obtain q2 where b_q2: "q2 = b div m" by blast

  have a_r1_q1: "a = m * q1 + r1"
    using a_r1 a_q1 by simp
  have b_r2_q2: "b = m * q2 + r2"
    using b_r2 b_q2 by simp

  have "b - a = m * q2 + r2 - (m * q1 + r1)"
    using a_r1_q1 b_r2_q2 by simp
  also have "… = m * q2 + r2 - m * q1 - r1"
    by simp
  also have "… = m * q2 - m * q1 + r2 - r1"
    by simp
  finally have "b - a = m * (q2 - q1) + (r2 - r1)"
    by (simp add: right_diff_distrib)
  hence "(b - a) mod m = (r2 - r1) mod m"
    by (simp add: mod_add_eq)
  hence r2_r1_mod_m_0:"(r2 - r1) mod m = 0" (is "?R1")
    by (simp only: as1)

  have "r1 = r2"
  proof (rule notI[of "r1 ≠ r2", simplified])
    assume as1': "r1 ≠ r2"
    have diff_le_s: "⋀a b (m::int). ⟦ 0 ≤ a; b < m ⟧ ⟹ b - a < m"
      by simp
    from as2 a_r1 b_r2 have s_r1:"0 ≤ r1 ∧ r1 < m" and s_r2:"0 ≤ r2 ∧ r2 < m"
      by simp_all
    have mr2r1:"-m < r2 - r1" and r2r1m:"r2 - r1 < m"
      by (simp add: minus_less_iff[of m] s_r1 s_r2 diff_le_s)+
    have "0 ≤ r2 - r1 ⟹ (r2 - r1) mod m = (r2 - r1)"
      using r2r1m by (blast intro: mod_pos_pos_trivial)
    hence s1_pos: "0 ≤ r2 - r1 ⟹ r2 - r1 = 0"
      using r2_r1_mod_m_0 by simp

    have "(r2-r1) mod -m = 0"
      by (simp add: zmod_zminus2_eq_if[of "r2-r1" m, simplified] r2_r1_mod_m_0)
    moreover
    have "r2 - r1 ≤ 0 ⟹ (r2 - r1) mod -m = r2 - r1"
      using mr2r1
      by (simp add: mod_neg_neg_trivial)
    ultimately have s1_neg:"r2 - r1 ≤ 0 ⟹ r2 - r1 = 0"
      by simp

    have "r2 - r1 = 0"
      using s1_pos s1_neg linorder_linear by blast
    hence "r1 = r2" by simp
    thus False
      using as1' by blast
  qed
  thus ?thesis
    using a_r1 b_r2 by blast
qed

lemma zmod_zminus_eq_conv_pos: "
  0 < (m::int) ⟹ (a mod - m = b mod - m) = (a mod m = b mod m)"
apply (simp only: mod_minus_right neg_equal_iff_equal)
apply (simp only: zmod_zminus1_eq_if)
apply (split if_split)+
apply (safe, simp_all)
apply (insert pos_mod_bound[of m a] pos_mod_bound[of m b], simp_all)
done
lemma zmod_zminus_eq_conv: "
  ((a::int) mod - m = b mod - m) = (a mod m = b mod m)"
apply (insert linorder_less_linear[of 0 m], elim disjE)
apply (blast dest: zmod_zminus_eq_conv_pos)
apply simp
apply (simp add: zmod_zminus_eq_conv_pos[of "-m", symmetric])
done

lemma zdiff_mod_0_imp_mod_eq:"
  (b - a) mod m = 0 ⟹ (a::int) mod m = b mod m"
by (metis dvd_eq_mod_eq_0 mod_eq_dvd_iff)

lemma zmod_eq_diff_mod_0_conv: "
  ((a::int) mod m = b mod m) = ((b - a) mod m = 0)"
apply (rule iffI)
apply (rule zmod_eq_imp_diff_mod_0, assumption)
apply (rule zdiff_mod_0_imp_mod_eq, assumption)
done

lemma "¬(∃(a::int) b m. (b - a) mod m = 0 ∧ a mod m ≠ b mod m)"
by (simp add: zmod_eq_diff_mod_0_conv)
lemma "∃(a::nat) b m. (b - a) mod m = 0 ∧ a mod m ≠ b mod m"
apply (rule_tac x=1 in exI)
apply (rule_tac x=0 in exI)
apply (rule_tac x=2 in exI)
apply simp
done



lemma zmult_div_leq_mono:"
  ⟦ (0::int) ≤ x; a ≤ b; 0 < d ⟧ ⟹ x * a div d ≤ x * b div d"
by (metis mult_right_mono zdiv_mono1 mult.commute)

lemma zmult_div_leq_mono_neg:"
  ⟦ x ≤ (0::int); a ≤ b; 0 < d ⟧ ⟹ x * b div d ≤ x * a div d"
by (metis mult_left_mono_neg zdiv_mono1)

lemma zmult_div_pos_le:"
  ⟦ (0::int) ≤ a; 0 ≤ b; b ≤ c ⟧ ⟹ a * b div c ≤ a"
apply (case_tac "b = 0", simp)
apply (subgoal_tac "b * a ≤ c * a")
 prefer 2
 apply (simp only: mult_right_mono)
apply (simp only: mult.commute)
apply (subgoal_tac "a * b div c ≤ a * c div c")
 prefer 2
 apply (simp only: zdiv_mono1)
apply simp
done

lemma zmult_div_neg_le:"
  ⟦ a ≤ (0::int); 0 < c; c ≤ b ⟧ ⟹ a * b div c ≤ a"
apply (subgoal_tac "b * a ≤ c * a")
 prefer 2
 apply (simp only: mult_right_mono_neg)
apply (simp only: mult.commute)
apply (subgoal_tac "a * b div c ≤ a * c div c")
 prefer 2
 apply (simp only: zdiv_mono1)
apply simp
done

lemma zmult_div_ge_0:"⟦ (0::int) ≤ x; 0 ≤ a; 0 < c ⟧ ⟹ 0 ≤ a * x div c"
by (metis pos_imp_zdiv_nonneg_iff split_mult_pos_le)

corollary zmult_div_plus_ge_0: "
  ⟦ (0::int) ≤ x; 0 ≤ a; 0 ≤ b; 0 < c⟧ ⟹ 0 ≤ a * x div c + b"
by (insert zmult_div_ge_0[of x a c], simp)


lemma zmult_div_abs_ge: "
  ⟦ (0::int) ≤ b; b ≤ b'; 0 ≤ a; 0 < c⟧ ⟹
  ¦a * b div c¦ ≤ ¦a * b' div c¦"
apply (insert zmult_div_ge_0[of b a c] zmult_div_ge_0[of "b'" a c], simp)
by (metis zmult_div_leq_mono)

lemma zmult_div_plus_abs_ge: "
  ⟦ (0::int) ≤ b; b ≤ b'; 0 ≤ a; 0 < c ⟧ ⟹
  ¦a * b div c + a¦ ≤ ¦a * b' div c + a¦"
apply (insert zmult_div_plus_ge_0[of b a a c] zmult_div_plus_ge_0[of "b'" a a c], simp)
by (metis zmult_div_leq_mono)


subsection ‹Some further (in-)equality results for ‹div› and ‹mod››

lemma less_mod_eq_imp_add_divisor_le: "
  ⟦ (x::nat) < y; x mod m = y mod m ⟧ ⟹ x + m ≤ y"
apply (case_tac "m = 0")
 apply simp
apply (rule contrapos_pp[of "x mod m = y mod m"])
 apply blast
apply (rule ccontr, simp only: not_not, clarify)
proof -
  assume m_greater_0: "0 < m"
  assume x_less_y:"x < y"
  hence y_x_greater_0:"0 < y - x"
    by simp
  assume "x mod m = y mod m"
  hence y_x_mod_m: "(y - x) mod m = 0"
    by (simp only: mod_eq_imp_diff_mod_0)
  assume "¬ x + m ≤ y"
  hence "y < x + m" by simp
  hence "y - x < x + m - x"
    by (simp add: diff_add_inverse diff_less_conv m_greater_0)
  hence y_x_less_m: "y - x < m"
    by simp
  have "(y - x) mod m = y - x"
    using y_x_less_m by simp
  hence "y - x = 0"
    using y_x_mod_m by simp
  thus False
    using y_x_greater_0 by simp
qed


lemma less_div_imp_mult_add_divisor_le: "
  (x::nat) < n div m ⟹ x * m + m ≤ n"
apply (case_tac "m = 0", simp)
apply (case_tac "n < m", simp)
apply (simp add: linorder_not_less)
apply (subgoal_tac "m ≤ n - n mod m")
 prefer 2
 apply (drule div_le_mono[of m _ m])
 apply (simp only: div_self)
 apply (drule mult_le_mono2[of 1 _ m])
 apply (simp only: mult_1_right minus_mod_eq_mult_div [symmetric])
apply (drule less_imp_le_pred[of x])
apply (drule mult_le_mono2[of x _ m])
apply (simp add: diff_mult_distrib2 minus_mod_eq_mult_div [symmetric] del: diff_diff_left)
apply (simp only: le_diff_conv2[of m])
apply (drule le_diff_imp_le[of "m * x + m"])
apply (simp only: mult.commute[of _ m])
done

lemma mod_add_eq_imp_mod_0: "
  ((n + k) mod (m::nat) = n mod m) = (k mod m = 0)"
by (metis add_eq_if mod_add mod_add_self1 mod_self add.commute)

lemma between_imp_mod_between: "
  ⟦ b < (m::nat); m * k + a ≤ n; n ≤ m * k + b ⟧ ⟹
  a ≤ n mod m ∧ n mod m ≤ b"
  apply (case_tac "m = 0", simp_all)
  apply (frule gr_implies_gr0)
  apply (subgoal_tac "k = n div m")
   prefer 2
   apply (rule sym, rule div_nat_eqI) apply simp
   apply simp
  apply clarify
  apply (rule conjI)
   apply (rule add_le_imp_le_left[where c="m * (n div m)"], simp)+
  done

corollary between_imp_mod_le: "
  ⟦ b < (m::nat); m * k ≤ n; n ≤ m * k + b ⟧ ⟹ n mod m ≤ b"
by (insert between_imp_mod_between[of b m k 0 n], simp)
corollary between_imp_mod_gr0: "
  ⟦ (m::nat) * k < n; n < m * k + m ⟧ ⟹ 0 < n mod m"
apply (case_tac "m = 0", simp_all)
apply (rule Suc_le_lessD)
apply (rule between_imp_mod_between[THEN conjunct1, of "m - Suc 0" m k "Suc 0" n])
apply simp_all
done

corollary le_less_div_conv: "
  0 < m ⟹ (k * m ≤ n ∧ n < Suc k * m) = (n div m = k)"
  by (auto simp add: ac_simps intro: div_nat_eqI dividend_less_times_div)

lemma le_less_imp_div: "
  ⟦ k * m ≤ n; n < Suc k * m ⟧ ⟹ n div m = k"
  by (auto simp add: ac_simps intro: div_nat_eqI)  

lemma div_imp_le_less: "
  ⟦ n div m = k; 0 < m ⟧ ⟹ k * m ≤ n ∧ n < Suc k * m"
  by (auto simp add: ac_simps intro: dividend_less_times_div)

lemma div_le_mod_le_imp_le: "
  ⟦ (a::nat) div m ≤ b div m; a mod m ≤ b mod m ⟧ ⟹ a ≤ b"
apply (rule subst[OF mult_div_mod_eq[of m a]])
apply (rule subst[OF mult_div_mod_eq[of m b]])
apply (rule add_le_mono)
apply (rule mult_le_mono2)
apply assumption+
done

lemma le_mod_add_eq_imp_add_mod_le: "
  ⟦ a ≤ b; (a + k) mod m = (b::nat) mod m ⟧ ⟹ a + k mod m ≤ b"
by (metis add_le_mono2 diff_add_inverse le_add1 le_add_diff_inverse mod_diff1_eq mod_less_eq_dividend)

corollary mult_divisor_le_mod_ge_imp_ge: "
  ⟦ (m::nat) * k ≤ n; r ≤ n mod m ⟧ ⟹ m * k + r ≤ n"
apply (insert le_mod_add_eq_imp_add_mod_le[of "m * k" n "n mod m" m])
apply (simp add: add.commute[of "m * k"])
done


subsection ‹Additional multiplication results for ‹mod› and ‹div››

lemma mod_0_imp_mod_mult_right_0: "
  n mod m = (0::nat) ⟹ n * k mod m = 0"
by fastforce
lemma mod_0_imp_mod_mult_left_0: "
  n mod m = (0::nat) ⟹ k * n mod m = 0"
by fastforce

lemma mod_0_imp_div_mult_left_eq: "
  n mod m = (0::nat) ⟹ k * n div m = k * (n div m)"
by fastforce
lemma mod_0_imp_div_mult_right_eq: "
  n mod m = (0::nat) ⟹ n * k div m = k * (n div m)"
by fastforce


lemma mod_0_imp_mod_factor_0_left: "
  n mod (m * m') = (0::nat) ⟹ n mod m = 0"
by fastforce
lemma mod_0_imp_mod_factor_0_right: "
  n mod (m * m') = (0::nat) ⟹ n mod m' = 0"
by fastforce


subsection ‹Some factor distribution facts for ‹mod››

lemma mod_eq_mult_distrib: "
  (a::nat) mod m = b mod m ⟹
  a * k mod (m * k) = b * k mod (m * k)"
by simp

lemma mod_mult_eq_imp_mod_eq: "
  (a::nat) mod (m * k) = b mod (m * k) ⟹ a mod m = b mod m"
apply (simp only: mod_mult2_eq)
apply (drule_tac arg_cong[where f="λx. x mod m"])
apply (simp add: add.commute)
done
corollary mod_eq_mod_0_imp_mod_eq: "
  ⟦ (a::nat) mod m' = b mod m'; m' mod m = 0 ⟧
  ⟹ a mod m = b mod m"
  using mod_mod_cancel [of m m' a] mod_mod_cancel [of m m' b] by auto

lemma mod_factor_imp_mod_0: "
  ⟦(x::nat) mod (m * k) = y * k mod (m * k)⟧ ⟹ x mod k = 0"
  (is "⟦ ?P1 ⟧ ⟹ ?Q")
proof -
  assume as1: ?P1
  have "y * k mod (m * k) = y mod m * k"
    by simp
  hence "x mod (m * k) = y mod m * k"
    using as1 by simp
  hence "y mod m * k = k * (x div k mod m) + x mod k" (is "?l1 = ?r1")
    by (simp only: ac_simps mod_mult2_eq)
  hence "(y mod m * k) mod k = ?r1 mod k"
    by simp
  hence "0 = ?r1 mod k"
    by simp
  thus "x mod k = 0"
    by (simp add: mod_add_eq)
qed
corollary mod_factor_div: "
  ⟦(x::nat) mod (m * k) = y * k mod (m * k)⟧ ⟹ x div k * k = x"
by (blast intro: mod_factor_imp_mod_0[THEN mod_0_div_mult_cancel[THEN iffD1]])

lemma mod_factor_div_mod:"
  ⟦ (x::nat) mod (m * k) = y * k mod (m * k); 0 < k ⟧
  ⟹ x div k mod m = y mod m"
  (is "⟦ ?P1; ?P2 ⟧ ⟹ ?L = ?R")
proof -
  assume as1: ?P1
  assume as2: ?P2
  have x_mod_k_0: "x mod k = 0"
    using as1 by (blast intro: mod_factor_imp_mod_0)
  have "?L * k + x mod k = x mod (k * m)"
    by (simp only: mod_mult2_eq mult.commute[of _ k])
  hence "?L * k = x mod (k * m)"
    using x_mod_k_0 by simp
  hence "?L * k = y * k mod (m * k)"
    using as1 by (simp only: ac_simps)
  hence "?L * k = y mod m * k"
    by (simp only: mult_mod_left)
  thus ?thesis
    using as2 by simp
qed


subsection ‹More results about quotient ‹div› with addition and subtraction›

lemma div_add1_eq_if: "0 < m ⟹
  (a + b) div (m::nat) = a div m + b div m + (
    if a mod m + b mod m < m then 0 else Suc 0)"
apply (simp only: div_add1_eq[of a b])
apply (rule arg_cong[of "(a mod m + b mod m) div m"])
apply (clarsimp simp: linorder_not_less)
apply (rule le_less_imp_div[of "Suc 0" m "a mod m + b mod m"], simp)
apply simp
apply (simp only: add_less_mono[OF mod_less_divisor mod_less_divisor])
done
corollary div_add1_eq1: "
  a mod m + b mod m < (m::nat) ⟹
  (a + b) div (m::nat) = a div m + b div m"
apply (case_tac "m = 0", simp)
apply (simp add: div_add1_eq_if)
done
corollary div_add1_eq1_mod_0_left: "
  a mod m = 0 ⟹ (a + b) div (m::nat) = a div m + b div m"
apply (case_tac "m = 0", simp)
apply (simp add: div_add1_eq1)
done
corollary div_add1_eq1_mod_0_right: "
  b mod m = 0 ⟹ (a + b) div (m::nat) = a div m + b div m"
by (fastforce simp: div_add1_eq1_mod_0_left)
corollary div_add1_eq2: "
  ⟦ 0 < m; (m::nat) ≤ a mod m + b mod m ⟧ ⟹
  (a + b) div (m::nat) = Suc (a div m + b div m)"
by (simp add: div_add1_eq_if)

lemma div_Suc: "
  0 < n ⟹ Suc m div n = (if Suc (m mod n) = n then Suc (m div n) else m div n)"
apply (drule Suc_leI, drule le_imp_less_or_eq)
apply (case_tac "n = Suc 0", simp)
apply (split if_split, intro conjI impI)
 apply (rule_tac t="Suc m" and s="m + 1" in subst, simp)
 apply (subst div_add1_eq2, simp+)
apply (insert le_neq_trans[OF mod_less_divisor[THEN Suc_leI, of n m]], simp)
apply (rule_tac t="Suc m" and s="m + 1" in subst, simp)
apply (subst div_add1_eq1, simp+)
done
lemma div_Suc': "
  0 < n ⟹ Suc m div n = (if m mod n < n - Suc 0 then m div n else Suc (m div n))"
apply (simp add: div_Suc)
apply (intro conjI impI)
 apply simp
apply (insert le_neq_trans[OF mod_less_divisor[THEN Suc_leI, of n m]], simp)
done

lemma div_diff1_eq_if: "
  (b - a) div (m::nat) =
  b div m - a div m - (if a mod m ≤ b mod m then 0 else Suc 0)"
apply (case_tac "m = 0", simp)
apply (case_tac "b < a")
 apply (frule less_imp_le[of b])
 apply (frule div_le_mono[of _ _ m])
 apply simp
apply (simp only: linorder_not_less neq0_conv)
proof -
  assume le_as: "a ≤ b"
    and m_as: "0 < m"
  have div_le:"a div m ≤ b div m"
    using le_as by (simp only: div_le_mono)
  have "b - a = b div m * m + b mod m - (a div m * m + a mod m)"
    by simp
  also have "… = b div m * m + b mod m - a div m * m - a mod m"
    by simp
  also have "… = b div m * m - a div m * m + b mod m - a mod m"
    by (simp only: diff_add_assoc2[OF mult_le_mono1[OF div_le]])
  finally have b_a_s1: "b - a = (b div m - a div m) * m + b mod m - a mod m"
    (is "?b_a = ?b_a1")
    by (simp only: diff_mult_distrib)
  hence b_a_div_s: "(b - a) div m =
    ((b div m - a div m) * m + b mod m - a mod m) div m"
    by (rule arg_cong)

  show ?thesis
  proof (cases "a mod m ≤ b mod m")
    case True
    hence as': "a mod m ≤ b mod m" .

    have "(b - a) div m = ?b_a1 div m"
      using b_a_div_s .
    also have "… = ((b div m - a div m) * m + (b mod m - a mod m)) div m"
      using as' by simp
    also have "… = b div m - a div m + (b mod m - a mod m) div m"
      apply (simp only: add.commute)
      by (simp only: div_mult_self1[OF less_imp_neq[OF m_as, THEN not_sym]])
    finally have b_a_div_s': "(b - a) div m = …" .
    have "(b mod m - a mod m) div m = 0"
      by (rule div_less, rule less_imp_diff_less,
          rule mod_less_divisor, rule m_as)
    thus ?thesis
      using b_a_div_s' as'
      by simp
  next
    case False
    hence as1': "¬ a mod m ≤ b mod m" .
    hence as': "b mod m < a mod m" by simp

    have a_div_less: "a div m < b div m"
      using le_as as'
      by (blast intro: le_mod_greater_imp_div_less)

    have "b div m - a div m = b div m - a div m - (Suc 0 - Suc 0)"
      by simp
    also have "… = b div m - a div m + Suc 0 - Suc 0"
      by simp
    also have "… = b div m - a div m - Suc 0 + Suc 0"
      by (simp only: diff_add_assoc2
        a_div_less[THEN zero_less_diff[THEN iffD2], THEN Suc_le_eq[THEN iffD2]])
    finally have b_a_div_s': "b div m - a div m = …" .

    have "(b - a) div m = ?b_a1 div m"
      using b_a_div_s .
    also have "… = ((b div m - a div m - Suc 0 + Suc 0) * m
      + b mod m - a mod m ) div m"
      using b_a_div_s' by (rule arg_cong)
    also have "… = ((b div m - a div m - Suc 0) * m
      + Suc 0 * m + b mod m - a mod m ) div m"
      by (simp only: add_mult_distrib)
    also have "… = ((b div m - a div m - Suc 0) * m
      + m + b mod m - a mod m ) div m"
      by simp
    also have "… = ((b div m - a div m - Suc 0) * m
      + (m + b mod m - a mod m) ) div m"
      by (simp only: add.assoc m_as
        diff_add_assoc[of "a mod m" "m + b mod m"]
        trans_le_add1[of "a mod m" m, OF mod_le_divisor])
    also have "… = b div m - a div m - Suc 0
      + (m + b mod m - a mod m) div m"
      by (simp only: add.commute div_mult_self1[OF less_imp_neq[OF m_as, THEN not_sym]])
    finally have b_a_div_s': "(b - a) div m = …" .

    have div_0_s: "(m + b mod m - a mod m) div m = 0"
      by (rule div_less, simp only: add_diff_less m_as as')
    show ?thesis
      by (simp add: as1' b_a_div_s' div_0_s)
  qed
qed

corollary div_diff1_eq: "
  (b - a) div (m::nat) =
  b div m - a div m - (m + a mod m - Suc (b mod m)) div m"
apply (case_tac "m = 0", simp)
apply (simp only: neq0_conv)
apply (rule subst[of
  "if a mod m ≤ b mod m then 0 else Suc 0"
  "(m + a mod m - Suc(b mod m)) div m"])
 prefer 2 apply (rule div_diff1_eq_if)
apply (split if_split, rule conjI)
 apply simp
apply (clarsimp simp: linorder_not_le)
apply (rule sym)
apply (drule Suc_le_eq[of "b mod m", THEN iffD2])
apply (simp only: diff_add_assoc)
apply (simp only: div_add_self1)
apply (simp add: less_imp_diff_less)
done

corollary div_diff1_eq1: "
  a mod m ≤ b mod m ⟹
  (b - a) div (m::nat) = b div m - a div m"
by (simp add: div_diff1_eq_if)
corollary div_diff1_eq1_mod_0: "
  a mod m = 0 ⟹
  (b - a) div (m::nat) = b div m - a div m"
by (simp add: div_diff1_eq1)
corollary div_diff1_eq2: "
  b mod m < a mod m ⟹
  (b - a) div (m::nat) = b div m - Suc (a div m)"
by (simp add: div_diff1_eq_if)


subsection ‹Further results about ‹div› and ‹mod››

subsubsection ‹Some auxiliary facts about ‹mod››

lemma diff_less_divisor_imp_sub_mod_eq: "
  ⟦ (x::nat) ≤ y; y - x < m ⟧ ⟹ x = y - (y - x) mod m"
by simp
lemma diff_ge_divisor_imp_sub_mod_less: "
  ⟦ (x::nat) ≤ y; m ≤ y - x; 0 < m ⟧ ⟹ x < y - (y - x) mod m"
apply (simp only: less_diff_conv)
apply (simp only: le_diff_conv2 add.commute[of m])
apply (rule less_le_trans[of _ "x + m"])
apply simp_all
done

lemma le_imp_sub_mod_le: "
  (x::nat) ≤ y ⟹ x ≤ y - (y - x) mod m"
apply (case_tac "m = 0", simp_all)
apply (case_tac "m ≤ y - x")
apply (drule diff_ge_divisor_imp_sub_mod_less[of x y m])
apply simp_all
done

lemma mod_less_diff_mod: "
  ⟦ n mod m < r; r ≤ m; r ≤ (n::nat) ⟧ ⟹
  (n - r) mod m = m + n mod m - r"
apply (case_tac "r = m")
 apply (simp add: mod_diff_self2)
apply (simp add: mod_diff1_eq[of r n m])
done

lemma mod_0_imp_mod_pred: "
  ⟦ 0 < (n::nat); n mod m = 0 ⟧ ⟹
  (n - Suc 0) mod m = m - Suc 0"
apply (case_tac "m = 0", simp_all)
apply (simp only: Suc_le_eq[symmetric])
apply (simp only: mod_diff1_eq)
apply (case_tac "m = Suc 0")
apply simp_all
done

lemma mod_pred: "
  0 < n ⟹
  (n - Suc 0) mod m = (
    if n mod m = 0 then m - Suc 0 else n mod m - Suc 0)"
apply (split if_split, rule conjI)
 apply (simp add: mod_0_imp_mod_pred)
apply clarsimp
apply (case_tac "m = Suc 0", simp)
apply (frule subst[OF Suc0_mod[symmetric], where P="λx. x ≤ n mod m"], simp)
apply (simp only: mod_diff1_eq1)
apply (simp add: Suc0_mod)
done
corollary mod_pred_Suc_mod: "
  0 < n ⟹ Suc ((n - Suc 0) mod m) mod m = n mod m"
apply (case_tac "m = 0", simp)
apply (simp add: mod_pred)
done
corollary diff_mod_pred: "
  a < b ⟹
  (b - Suc a) mod m = (
    if a mod m = b mod m then m - Suc 0 else (b - a) mod m - Suc 0)"
apply (rule_tac t="b - Suc a" and s="b - a - Suc 0" in subst, simp)
apply (subst mod_pred, simp)
apply (simp add: mod_eq_diff_mod_0_conv)
done
corollary diff_mod_pred_Suc_mod: "
  a < b ⟹ Suc ((b - Suc a) mod m) mod m = (b - a) mod m"
apply (case_tac "m = 0", simp)
apply (simp add: diff_mod_pred mod_eq_diff_mod_0_conv)
done

lemma mod_eq_imp_diff_mod_eq_divisor: "
  ⟦ a < b; 0 < m; a mod m = b mod m ⟧ ⟹
  Suc ((b - Suc a) mod m) = m"
apply (drule mod_eq_imp_diff_mod_0[of a])
apply (frule iffD2[OF zero_less_diff])
apply (drule mod_0_imp_mod_pred[of "b-a" m], assumption)
apply simp
done


lemma sub_diff_mod_eq: "
  r ≤ t ⟹ (t - (t - r) mod m) mod (m::nat) = r mod m"
by (metis mod_diff_right_eq diff_diff_cancel diff_le_self)

lemma sub_diff_mod_eq': "
  r ≤ t ⟹ (k * m + t - (t - r) mod m) mod (m::nat) = r mod m"
apply (simp only: diff_mod_le[of t r m, THEN add_diff_assoc, symmetric])
apply (simp add: sub_diff_mod_eq)
done

lemma mod_eq_Suc_0_conv: "Suc 0 < k ⟹ ((x + k - Suc 0) mod k = 0) = (x mod k = Suc 0)"
apply (simp only: mod_pred)
apply (case_tac "x mod k = Suc 0")
apply simp_all
done

lemma mod_eq_divisor_minus_Suc_0_conv: "Suc 0 < k ⟹ (x mod k = k - Suc 0) = (Suc x mod k = 0)"
by (simp only: mod_Suc, split if_split, fastforce)


subsubsection ‹Some auxiliary facts about ‹div››

lemma sub_mod_div_eq_div: "((n::nat) - n mod m) div m = n div m"
apply (case_tac "m = 0", simp)
apply (simp add: minus_mod_eq_mult_div)
done

lemma mod_less_imp_diff_div_conv: "
  ⟦ n mod m < r; r ≤ m + n mod m⟧ ⟹ (n - r) div m = n div m - Suc 0"
  apply (case_tac "m = 0", simp)
  apply (simp only: neq0_conv)
  apply (case_tac "n < m", simp)
  apply (simp only: linorder_not_less)
  apply (rule div_nat_eqI)
   apply (simp_all add: algebra_simps minus_mod_eq_mult_div [symmetric])
  done

corollary mod_0_le_imp_diff_div_conv: "
  ⟦ n mod m = 0; 0 < r; r ≤ m ⟧ ⟹ (n - r) div m = n div m - Suc 0"
by (simp add: mod_less_imp_diff_div_conv)
corollary mod_0_less_imp_diff_Suc_div_conv: "
  ⟦ n mod m = 0; r < m ⟧ ⟹ (n - Suc r) div m = n div m - Suc 0"
by (drule mod_0_le_imp_diff_div_conv[where r="Suc r"], simp_all)
corollary mod_0_imp_diff_Suc_div_conv: "
  (n - r) mod m = 0 ⟹ (n - Suc r) div m = (n - r) div m - Suc 0"
apply (case_tac "m = 0", simp)
apply (rule_tac t="n - Suc r" and s="n - r - Suc 0" in subst, simp)
apply (rule mod_0_le_imp_diff_div_conv, simp+)
done
corollary mod_0_imp_sub_1_div_conv: "
  n mod m = 0 ⟹ (n - Suc 0) div m = n div m - Suc 0"
apply (case_tac "m = 0", simp)
apply (simp add: mod_0_less_imp_diff_Suc_div_conv)
done
corollary sub_Suc_mod_div_conv: "
  (n - Suc (n mod m)) div m = n div m - Suc 0"
apply (case_tac "m = 0", simp)
apply (simp add: mod_less_imp_diff_div_conv)
done


lemma div_le_conv: "0 < m ⟹ n div m ≤ k = (n ≤ Suc k * m - Suc 0)"
apply (rule iffI)
 apply (drule mult_le_mono1[of _ _ m])
 apply (simp only: mult.commute[of _ m] minus_mod_eq_mult_div [symmetric])
 apply (drule le_diff_conv[THEN iffD1])
 apply (rule le_trans[of _ "m * k + n mod m"], assumption)
 apply (simp add: add.commute[of m])
 apply (simp only: diff_add_assoc[OF Suc_leI])
 apply (rule add_le_mono[OF le_refl])
 apply (rule less_imp_le_pred)
 apply (rule mod_less_divisor, assumption)
apply (drule div_le_mono[of _ _ m])
apply (simp add: mod_0_imp_sub_1_div_conv)
done

lemma le_div_conv: "0 < (m::nat) ⟹ (n ≤ k div m) = (n * m ≤ k)"
apply (rule iffI)
 apply (drule mult_le_mono1[of _ _ m])
 apply (simp add: div_mult_cancel)
apply (drule div_le_mono[of _ _ m])
apply simp
done

lemma less_mult_imp_div_less: "n < k * m ⟹ n div m < (k::nat)"
apply (case_tac "k = 0", simp)
apply (case_tac "m = 0", simp)
apply simp
apply (drule less_imp_le_pred[of n])
apply (drule div_le_mono[of _ _ m])
apply (simp add: mod_0_imp_sub_1_div_conv)
done

lemma div_less_imp_less_mult: "⟦ 0 < (m::nat); n div m < k ⟧ ⟹ n < k * m"
apply (rule ccontr, simp only: linorder_not_less)
apply (drule div_le_mono[of _ _ m])
apply simp
done

lemma div_less_conv: "0 < (m::nat) ⟹ (n div m < k) = (n < k * m)"
apply (rule iffI)
apply (rule div_less_imp_less_mult, assumption+)
apply (rule less_mult_imp_div_less, assumption)
done

lemma div_eq_0_conv: "(n div (m::nat) = 0) = (m = 0 ∨ n < m)"
apply (rule iffI)
 apply (case_tac "m = 0", simp)
 apply (rule ccontr)
 apply (simp add: linorder_not_less)
 apply (drule div_le_mono[of _ _ m])
 apply simp
apply fastforce
done
lemma div_eq_0_conv': "0 < m ⟹ (n div (m::nat) = 0) = (n < m)"
by (simp add: div_eq_0_conv)
corollary div_gr_imp_gr_divisor: "x < n div (m::nat) ⟹ m ≤ n"
apply (drule gr_implies_gr0, drule neq0_conv[THEN iffD2])
apply (simp add: div_eq_0_conv)
done

lemma mod_0_less_div_conv: "
  n mod (m::nat) = 0 ⟹ (k * m < n) = (k < n div m)"
apply (case_tac "m = 0", simp)
apply fastforce
done

lemma add_le_divisor_imp_le_Suc_div: "
  ⟦ x div m ≤ n; y ≤ m ⟧ ⟹ (x + y) div m ≤ Suc n"
apply (case_tac "m = 0", simp)
apply (simp only: div_add1_eq_if[of _ x])
apply (drule order_le_less[of y, THEN iffD1], fastforce)
done


text ‹List of definitions and lemmas›

thm
  minus_mod_eq_mult_div [symmetric]
  mod_0_div_mult_cancel
  div_mult_le
  less_div_Suc_mult
thm
  Suc0_mod
  Suc0_mod_subst
  Suc0_mod_cong

thm
  mod_Suc_conv

thm
  mod_add
  mod_sub_add

thm
  mod_sub_eq_mod_0_conv
  mod_sub_eq_mod_swap

thm
  le_mod_greater_imp_div_less
thm
  mod_diff_right_eq
  mod_eq_imp_diff_mod_eq

thm
  divisor_add_diff_mod_if
  divisor_add_diff_mod_eq1
  divisor_add_diff_mod_eq2

thm
  mod_add_eq
  mod_add1_eq_if
thm
  mod_diff1_eq_if
  mod_diff1_eq
  mod_diff1_eq1
  mod_diff1_eq2

thm
  nat_mod_distrib
  int_mod_distrib

thm
  zmod_zminus_eq_conv

thm
  mod_eq_imp_diff_mod_0
  zmod_eq_imp_diff_mod_0

thm
  mod_neq_imp_diff_mod_neq0
  diff_mod_0_imp_mod_eq
  zdiff_mod_0_imp_mod_eq

thm
  zmod_eq_diff_mod_0_conv
  mod_eq_diff_mod_0_conv

thm
  less_mod_eq_imp_add_divisor_le
thm
  mod_add_eq_imp_mod_0
thm
  mod_eq_mult_distrib
  mod_factor_imp_mod_0
  mod_factor_div
  mod_factor_div_mod


thm
  mod_diff_self1
  mod_diff_self2
  mod_diff_mult_self1
  mod_diff_mult_self2

thm
  div_diff_self1
  div_diff_self2
  div_diff_mult_self1
  div_diff_mult_self2

thm
  le_less_imp_div
  div_imp_le_less
thm
  le_less_div_conv

thm
  diff_less_divisor_imp_sub_mod_eq
  diff_ge_divisor_imp_sub_mod_less
  le_imp_sub_mod_le

thm
  sub_mod_div_eq_div

thm
  mod_less_imp_diff_div_conv
  mod_0_le_imp_diff_div_conv
  mod_0_less_imp_diff_Suc_div_conv
  mod_0_imp_sub_1_div_conv


thm
  sub_Suc_mod_div_conv

thm
  mod_less_diff_mod
  mod_0_imp_mod_pred

thm
  mod_pred
  mod_pred_Suc_mod

thm
  mod_eq_imp_diff_mod_eq_divisor

thm
  diff_mod_le
  sub_diff_mod_eq
  sub_diff_mod_eq'

thm
  div_diff1_eq_if
  div_diff1_eq
  div_diff1_eq1
  div_diff1_eq2


thm
  div_le_conv

end