# Theory IntDiv

Up to index of Isabelle/ZF

theory IntDiv
imports IntArith OrderArith
begin

    (*  Title:      ZF/IntDiv.thy
        ID:         $Id: IntDiv.thy,v 1.12 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1999  University of Cambridge

    Here is the division algorithm in ML:

        fun posDivAlg (a,b) =
          if a<b then (0,a)
          else let val (q,r) = posDivAlg(a, 2*b)
                   in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
               end

        fun negDivAlg (a,b) =
          if 0<=a+b then (~1,a+b)
          else let val (q,r) = negDivAlg(a, 2*b)
                   in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
               end;

        fun negateSnd (q,r:int) = (q,~r);

        fun divAlg (a,b) = if 0<=a then
                              if b>0 then posDivAlg (a,b)
                               else if a=0 then (0,0)
                                    else negateSnd (negDivAlg (~a,~b))
                           else
                              if 0<b then negDivAlg (a,b)
                              else        negateSnd (posDivAlg (~a,~b));

    *)

    header{*The Division Operators Div and Mod*}

    theory IntDiv imports IntArith OrderArith begin

    constdefs
      quorem :: "[i,i] => o"
        "quorem == %<a,b> <q,r>.
                          a = b$*q $+ r &
                          (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"

      adjust :: "[i,i] => i"
        "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
                              else <#2$*q,r>"

    (** the division algorithm **)

    constdefs posDivAlg :: "i => i"
    (*for the case a>=0, b>0*)
    (*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
        "posDivAlg(ab) ==
           wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
                 ab,
                 %<a,b> f. if (a$<b | b$<=#0) then <#0,a>
                           else adjust(b, f ` <a,#2$*b>))"

    (*for the case a<0, b>0*)
    constdefs negDivAlg :: "i => i"
    (*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*)
        "negDivAlg(ab) ==
           wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
                 ab,
                 %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b>
                           else adjust(b, f ` <a,#2$*b>))"

    (*for the general case b≠0*)

    constdefs
      negateSnd :: "i => i"
        "negateSnd == %<q,r>. <q, $-r>"

      (*The full division algorithm considers all possible signs for a, b
        including the special case a=0, b<0, because negDivAlg requires a<0*)
      divAlg :: "i => i"
        "divAlg ==
           %<a,b>. if #0 $<= a then
                      if #0 $<= b then posDivAlg (<a,b>)
                      else if a=#0 then <#0,#0>
                           else negateSnd (negDivAlg (<$-a,$-b>))
                   else
                      if #0$<b then negDivAlg (<a,b>)
                      else         negateSnd (posDivAlg (<$-a,$-b>))"

      zdiv  :: "[i,i]=>i"                    (infixl "zdiv" 70)
        "a zdiv b == fst (divAlg (<intify(a), intify(b)>))"

      zmod  :: "[i,i]=>i"                    (infixl "zmod" 70)
        "a zmod b == snd (divAlg (<intify(a), intify(b)>))"

    (** Some basic laws by Sidi Ehmety (need linear arithmetic!) **)

    lemma zspos_add_zspos_imp_zspos: "[| #0 $< x;  #0 $< y |] ==> #0 $< x $+ y"
    apply (rule_tac y = "y" in zless_trans)
    apply (rule_tac [2] zdiff_zless_iff [THEN iffD1])
    apply auto
    done

    lemma zpos_add_zpos_imp_zpos: "[| #0 $<= x;  #0 $<= y |] ==> #0 $<= x $+ y"
    apply (rule_tac y = "y" in zle_trans)
    apply (rule_tac [2] zdiff_zle_iff [THEN iffD1])
    apply auto
    done

    lemma zneg_add_zneg_imp_zneg: "[| x $< #0;  y $< #0 |] ==> x $+ y $< #0"
    apply (rule_tac y = "y" in zless_trans)
    apply (rule zless_zdiff_iff [THEN iffD1])
    apply auto
    done

    (* this theorem is used below *)
    lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
         "[| x $<= #0;  y $<= #0 |] ==> x $+ y $<= #0"
    apply (rule_tac y = "y" in zle_trans)
    apply (rule zle_zdiff_iff [THEN iffD1])
    apply auto
    done

    lemma zero_lt_zmagnitude: "[| #0 $< k; k ∈ int |] ==> 0 < zmagnitude(k)"
    apply (drule zero_zless_imp_znegative_zminus)
    apply (drule_tac [2] zneg_int_of)
    apply (auto simp add: zminus_equation [of k])
    apply (subgoal_tac "0 < zmagnitude ($# succ (n))")
     apply simp
    apply (simp only: zmagnitude_int_of)
    apply simp
    done

    (*** Inequality lemmas involving $#succ(m) ***)

    lemma zless_add_succ_iff:
         "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"
    apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
    apply (rule_tac [3] x = "0" in bexI)
    apply (cut_tac m = "m" in int_succ_int_1)
    apply (cut_tac m = "n" in int_succ_int_1)
    apply simp
    apply (erule natE)
    apply auto
    apply (rule_tac x = "succ (n) " in bexI)
    apply auto
    done

    lemma zadd_succ_lemma:
         "z ∈ int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
    apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
    apply (auto intro: zle_anti_sym elim: zless_asym
                simp add: zless_imp_zle not_zless_iff_zle)
    done

    lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
    apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
    apply auto
    done

    (** Inequality reasoning **)

    lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)"
    apply (subgoal_tac "#1 = $# 1")
    apply (simp only: zless_add_succ_iff zle_def)
    apply auto
    done

    lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)"
    apply (subgoal_tac "#1 = $# 1")
    apply (simp only: zadd_succ_zle_iff)
    apply auto
    done

    lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)"
    apply (subst zadd_commute)
    apply (rule add1_zle_iff)
    done

    (*** Monotonicity of Multiplication ***)

    lemma zmult_mono_lemma: "k ∈ nat ==> i $<= j ==> i $* $#k $<= j $* $#k"
    apply (induct_tac "k")
     prefer 2 apply (subst int_succ_int_1)
    apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono)
    done

    lemma zmult_zle_mono1: "[| i $<= j;  #0 $<= k |] ==> i$*k $<= j$*k"
    apply (subgoal_tac "i $* intify (k) $<= j $* intify (k) ")
    apply (simp (no_asm_use))
    apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
    apply (rule_tac [3] zmult_mono_lemma)
    apply auto
    apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym])
    done

    lemma zmult_zle_mono1_neg: "[| i $<= j;  k $<= #0 |] ==> j$*k $<= i$*k"
    apply (rule zminus_zle_zminus [THEN iffD1])
    apply (simp del: zmult_zminus_right
                add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
    done

    lemma zmult_zle_mono2: "[| i $<= j;  #0 $<= k |] ==> k$*i $<= k$*j"
    apply (drule zmult_zle_mono1)
    apply (simp_all add: zmult_commute)
    done

    lemma zmult_zle_mono2_neg: "[| i $<= j;  k $<= #0 |] ==> k$*j $<= k$*i"
    apply (drule zmult_zle_mono1_neg)
    apply (simp_all add: zmult_commute)
    done

    (* $<= monotonicity, BOTH arguments*)
    lemma zmult_zle_mono:
         "[| i $<= j;  k $<= l;  #0 $<= j;  #0 $<= k |] ==> i$*k $<= j$*l"
    apply (erule zmult_zle_mono1 [THEN zle_trans])
    apply assumption
    apply (erule zmult_zle_mono2)
    apply assumption
    done

    (** strict, in 1st argument; proof is by induction on k>0 **)

    lemma zmult_zless_mono2_lemma [rule_format]:
         "[| i$<j; k ∈ nat |] ==> 0<k --> $#k $* i $< $#k $* j"
    apply (induct_tac "k")
     prefer 2
     apply (subst int_succ_int_1)
     apply (erule natE)
    apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
    apply (frule nat_0_le)
    apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ")
    apply (simp (no_asm_use))
    apply (rule zadd_zless_mono)
    apply (simp_all (no_asm_simp) add: zle_def)
    done

    lemma zmult_zless_mono2: "[| i$<j;  #0 $< k |] ==> k$*i $< k$*j"
    apply (subgoal_tac "intify (k) $* i $< intify (k) $* j")
    apply (simp (no_asm_use))
    apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
    apply (rule_tac [3] zmult_zless_mono2_lemma)
    apply auto
    apply (simp add: znegative_iff_zless_0)
    apply (drule zless_trans, assumption)
    apply (auto simp add: zero_lt_zmagnitude)
    done

    lemma zmult_zless_mono1: "[| i$<j;  #0 $< k |] ==> i$*k $< j$*k"
    apply (drule zmult_zless_mono2)
    apply (simp_all add: zmult_commute)
    done

    (* < monotonicity, BOTH arguments*)
    lemma zmult_zless_mono:
         "[| i $< j;  k $< l;  #0 $< j;  #0 $< k |] ==> i$*k $< j$*l"
    apply (erule zmult_zless_mono1 [THEN zless_trans])
    apply assumption
    apply (erule zmult_zless_mono2)
    apply assumption
    done

    lemma zmult_zless_mono1_neg: "[| i $< j;  k $< #0 |] ==> j$*k $< i$*k"
    apply (rule zminus_zless_zminus [THEN iffD1])
    apply (simp del: zmult_zminus_right
                add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
    done

    lemma zmult_zless_mono2_neg: "[| i $< j;  k $< #0 |] ==> k$*j $< k$*i"
    apply (rule zminus_zless_zminus [THEN iffD1])
    apply (simp del: zmult_zminus
                add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
    done

    (** Products of zeroes **)

    lemma zmult_eq_lemma:
         "[| m ∈ int; n ∈ int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)"
    apply (case_tac "m $< #0")
    apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
    apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
    done

    lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"
    apply (simp add: zmult_eq_lemma)
    done

    (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
        but not (yet?) for k*m < n*k. **)

    lemma zmult_zless_lemma:
         "[| k ∈ int; m ∈ int; n ∈ int |]
          ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
    apply (case_tac "k = #0")
    apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
    apply (auto simp add: not_zless_iff_zle
                          not_zle_iff_zless [THEN iff_sym, of "m$*k"]
                          not_zle_iff_zless [THEN iff_sym, of m])
    apply (auto elim: notE
                simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
    done

    lemma zmult_zless_cancel2:
         "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
    apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
           in zmult_zless_lemma)
    apply auto
    done

    lemma zmult_zless_cancel1:
         "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
    by (simp add: zmult_commute [of k] zmult_zless_cancel2)

    lemma zmult_zle_cancel2:
         "(m$*k $<= n$*k) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))"
    by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)

    lemma zmult_zle_cancel1:
         "(k$*m $<= k$*n) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))"
    by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)

    lemma int_eq_iff_zle: "[| m ∈ int; n ∈ int |] ==> m=n <-> (m $<= n & n $<= m)"
    apply (blast intro: zle_refl zle_anti_sym)
    done

    lemma zmult_cancel2_lemma:
         "[| k ∈ int; m ∈ int; n ∈ int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)"
    apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
    apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
    done

    lemma zmult_cancel2 [simp]:
         "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"
    apply (rule iff_trans)
    apply (rule_tac [2] zmult_cancel2_lemma)
    apply auto
    done

    lemma zmult_cancel1 [simp]:
         "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"
    by (simp add: zmult_commute [of k] zmult_cancel2)

    subsection{* Uniqueness and monotonicity of quotients and remainders *}

    lemma unique_quotient_lemma:
         "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |]
          ==> q' $<= q"
    apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r")
     prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
    apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ")
     prefer 2
     apply (erule zle_zless_trans)
     apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
     apply (erule zle_zless_trans)
     apply (simp add: );
    apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)")
     prefer 2
     apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
    apply (auto elim: zless_asym
            simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls)
    done

    lemma unique_quotient_lemma_neg:
         "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |]
          ==> q $<= q'"
    apply (rule_tac b = "$-b" and r = "$-r'" and r' = "$-r"
           in unique_quotient_lemma)
    apply (auto simp del: zminus_zadd_distrib
                simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus)
    done

    lemma unique_quotient:
         "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b ∈ int; b ~= #0;
             q ∈ int; q' ∈ int |] ==> q = q'"
    apply (simp add: split_ifs quorem_def neq_iff_zless)
    apply safe
    apply simp_all
    apply (blast intro: zle_anti_sym
                 dest: zle_eq_refl [THEN unique_quotient_lemma]
                       zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+
    done

    lemma unique_remainder:
         "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b ∈ int; b ~= #0;
             q ∈ int; q' ∈ int;
             r ∈ int; r' ∈ int |] ==> r = r'"
    apply (subgoal_tac "q = q'")
     prefer 2 apply (blast intro: unique_quotient)
    apply (simp add: quorem_def)
    done

    subsection{*Correctness of posDivAlg,
               the Division Algorithm for @{text "a≥0"} and @{text "b>0"} *}

    lemma adjust_eq [simp]:
         "adjust(b, <q,r>) = (let diff = r$-b in
                              if #0 $<= diff then <#2$*q $+ #1,diff>
                                             else <#2$*q,r>)"
    by (simp add: Let_def adjust_def)

    lemma posDivAlg_termination:
         "[| #0 $< b; ~ a $< b |]
          ==> nat_of(a $- #2 $× b $+ #1) < nat_of(a $- b $+ #1)"
    apply (simp (no_asm) add: zless_nat_conj)
    apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
    done

    lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure]

    lemma posDivAlg_eqn:
         "[| #0 $< b; a ∈ int; b ∈ int |] ==>
          posDivAlg(<a,b>) =
           (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))"
    apply (rule posDivAlg_unfold [THEN trans])
    apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym])
    apply (blast intro: posDivAlg_termination)
    done

    lemma posDivAlg_induct_lemma [rule_format]:
      assumes prem:
            "!!a b. [| a ∈ int; b ∈ int;
                       ~ (a $< b | b $<= #0) --> P(<a, #2 $* b>) |] ==> P(<a,b>)"
      shows "<u,v> ∈ int*int --> P(<u,v>)"
    apply (rule_tac a = "<u,v>" in wf_induct)
    apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"
           in wf_measure)
    apply clarify
    apply (rule prem)
    apply (drule_tac [3] x = "<xa, #2 $× y>" in spec)
    apply auto
    apply (simp add: not_zle_iff_zless posDivAlg_termination)
    done

    lemma posDivAlg_induct:
      assumes u_int: "u ∈ int"
          and v_int: "v ∈ int"
          and ih: "!!a b. [| a ∈ int; b ∈ int;
                         ~ (a $< b | b $<= #0) --> P(a, #2 $* b) |] ==> P(a,b)"
      shows "P(u,v)"
    apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
    apply simp
    apply (rule posDivAlg_induct_lemma)
    apply (simp (no_asm_use))
    apply (rule ih)
    apply (auto simp add: u_int v_int)
    done

    (*FIXME: use intify in integ_of so that we always have integ_of w ∈ int.
        then this rewrite can work for ALL constants!!*)
    lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m $<= #0 & #0 $<= m)"
    apply (simp (no_asm) add: int_eq_iff_zle)
    done

    subsection{* Some convenient biconditionals for products of signs *}

    lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
    apply (drule zmult_zless_mono1)
    apply auto
    done

    lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"
    apply (drule zmult_zless_mono1_neg)
    apply auto
    done

    lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0"
    apply (drule zmult_zless_mono1_neg)
    apply auto
    done

    (** Inequality reasoning **)

    lemma int_0_less_lemma:
         "[| x ∈ int; y ∈ int |]
          ==> (#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
    apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
    apply (rule ccontr)
    apply (rule_tac [2] ccontr)
    apply (auto simp add: zle_def not_zless_iff_zle)
    apply (erule_tac P = "#0$< x$* y" in rev_mp)
    apply (erule_tac [2] P = "#0$< x$* y" in rev_mp)
    apply (drule zmult_pos_neg, assumption)
     prefer 2
     apply (drule zmult_pos_neg, assumption)
    apply (auto dest: zless_not_sym simp add: zmult_commute)
    done

    lemma int_0_less_mult_iff:
         "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
    apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
    apply auto
    done

    lemma int_0_le_lemma:
         "[| x ∈ int; y ∈ int |]
          ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
    by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)

    lemma int_0_le_mult_iff:
         "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
    apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
    apply auto
    done

    lemma zmult_less_0_iff:
         "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
    apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
    apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
    done

    lemma zmult_le_0_iff:
         "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
    by (auto dest: zless_not_sym
             simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])

    (*Typechecking for posDivAlg*)
    lemma posDivAlg_type [rule_format]:
         "[| a ∈ int; b ∈ int |] ==> posDivAlg(<a,b>) ∈ int * int"
    apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
    apply assumption+
    apply (case_tac "#0 $< ba")
     apply (simp add: posDivAlg_eqn adjust_def integ_of_type
                 split add: split_if_asm)
     apply clarify
     apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
    apply (simp add: not_zless_iff_zle)
    apply (subst posDivAlg_unfold)
    apply simp
    done

    (*Correctness of posDivAlg: it computes quotients correctly*)
    lemma posDivAlg_correct [rule_format]:
         "[| a ∈ int; b ∈ int |]
          ==> #0 $<= a --> #0 $< b --> quorem (<a,b>, posDivAlg(<a,b>))"
    apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
    apply auto
       apply (simp_all add: quorem_def)
       txt{*base case: a<b*}
       apply (simp add: posDivAlg_eqn)
      apply (simp add: not_zless_iff_zle [THEN iff_sym])
     apply (simp add: int_0_less_mult_iff)
    txt{*main argument*}
    apply (subst posDivAlg_eqn)
    apply (simp_all (no_asm_simp))
    apply (erule splitE)
    apply (rule posDivAlg_type)
    apply (simp_all add: int_0_less_mult_iff)
    apply (auto simp add: zadd_zmult_distrib2 Let_def)
    txt{*now just linear arithmetic*}
    apply (simp add: not_zle_iff_zless zdiff_zless_iff)
    done

    subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}

    lemma negDivAlg_termination:
         "[| #0 $< b; a $+ b $< #0 |]
          ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)"
    apply (simp (no_asm) add: zless_nat_conj)
    apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym]
                     zless_zminus)
    done

    lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure]

    lemma negDivAlg_eqn:
         "[| #0 $< b; a : int; b : int |] ==>
          negDivAlg(<a,b>) =
           (if #0 $<= a$+b then <#-1,a$+b>
                           else adjust(b, negDivAlg (<a, #2$*b>)))"
    apply (rule negDivAlg_unfold [THEN trans])
    apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym])
    apply (blast intro: negDivAlg_termination)
    done

    lemma negDivAlg_induct_lemma [rule_format]:
      assumes prem:
            "!!a b. [| a ∈ int; b ∈ int;
                       ~ (#0 $<= a $+ b | b $<= #0) --> P(<a, #2 $* b>) |]
                    ==> P(<a,b>)"
      shows "<u,v> ∈ int*int --> P(<u,v>)"
    apply (rule_tac a = "<u,v>" in wf_induct)
    apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"
           in wf_measure)
    apply clarify
    apply (rule prem)
    apply (drule_tac [3] x = "<xa, #2 $× y>" in spec)
    apply auto
    apply (simp add: not_zle_iff_zless negDivAlg_termination)
    done

    lemma negDivAlg_induct:
      assumes u_int: "u ∈ int"
          and v_int: "v ∈ int"
          and ih: "!!a b. [| a ∈ int; b ∈ int;
                             ~ (#0 $<= a $+ b | b $<= #0) --> P(a, #2 $* b) |]
                          ==> P(a,b)"
      shows "P(u,v)"
    apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
    apply simp
    apply (rule negDivAlg_induct_lemma)
    apply (simp (no_asm_use))
    apply (rule ih)
    apply (auto simp add: u_int v_int)
    done

    (*Typechecking for negDivAlg*)
    lemma negDivAlg_type:
         "[| a ∈ int; b ∈ int |] ==> negDivAlg(<a,b>) ∈ int * int"
    apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
    apply assumption+
    apply (case_tac "#0 $< ba")
     apply (simp add: negDivAlg_eqn adjust_def integ_of_type
                 split add: split_if_asm)
     apply clarify
     apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
    apply (simp add: not_zless_iff_zle)
    apply (subst negDivAlg_unfold)
    apply simp
    done

    (*Correctness of negDivAlg: it computes quotients correctly
      It doesn't work if a=0 because the 0/b=0 rather than -1*)
    lemma negDivAlg_correct [rule_format]:
         "[| a ∈ int; b ∈ int |]
          ==> a $< #0 --> #0 $< b --> quorem (<a,b>, negDivAlg(<a,b>))"
    apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
      apply auto
       apply (simp_all add: quorem_def)
       txt{*base case: @{term "0$<=a$+b"}*}
       apply (simp add: negDivAlg_eqn)
      apply (simp add: not_zless_iff_zle [THEN iff_sym])
     apply (simp add: int_0_less_mult_iff)
    txt{*main argument*}
    apply (subst negDivAlg_eqn)
    apply (simp_all (no_asm_simp))
    apply (erule splitE)
    apply (rule negDivAlg_type)
    apply (simp_all add: int_0_less_mult_iff)
    apply (auto simp add: zadd_zmult_distrib2 Let_def)
    txt{*now just linear arithmetic*}
    apply (simp add: not_zle_iff_zless zdiff_zless_iff)
    done

    subsection{* Existence shown by proving the division algorithm to be correct *}

    (*the case a=0*)
    lemma quorem_0: "[|b ≠ #0;  b ∈ int|] ==> quorem (<#0,b>, <#0,#0>)"
    by (force simp add: quorem_def neq_iff_zless)

    lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
    apply (subst posDivAlg_unfold)
    apply simp
    done

    lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
    apply (subst posDivAlg_unfold)
    apply (simp add: not_zle_iff_zless)
    done

    (*Needed below.  Actually it's an equivalence.*)
    lemma linear_arith_lemma: "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)"
    apply (simp add: not_zle_iff_zless)
    apply (drule zminus_zless_zminus [THEN iffD2])
    apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus)
    done

    lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b$-#1>"
    apply (subst negDivAlg_unfold)
    apply (simp add: linear_arith_lemma integ_of_type vimage_iff)
    done

    lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, $-r>"
    apply (unfold negateSnd_def)
    apply auto
    done

    lemma negateSnd_type: "qr ∈ int * int ==> negateSnd (qr) ∈ int * int"
    apply (unfold negateSnd_def)
    apply auto
    done

    lemma quorem_neg:
         "[|quorem (<$-a,$-b>, qr);  a ∈ int;  b ∈ int;  qr ∈ int * int|]
          ==> quorem (<a,b>, negateSnd(qr))"
    apply clarify
    apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
    txt{*linear arithmetic from here on*}
    apply (simp_all add: zminus_equation [of a] zminus_zless)
    apply (cut_tac [2] z = "b" and w = "#0" in zless_linear)
    apply (cut_tac [1] z = "b" and w = "#0" in zless_linear)
    apply auto
    apply (blast dest: zle_zless_trans)+
    done

    lemma divAlg_correct:
         "[|b ≠ #0;  a ∈ int;  b ∈ int|] ==> quorem (<a,b>, divAlg(<a,b>))"
    apply (auto simp add: quorem_0 divAlg_def)
    apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
                        posDivAlg_type negDivAlg_type)
    apply (auto simp add: quorem_def neq_iff_zless)
    txt{*linear arithmetic from here on*}
    apply (auto simp add: zle_def)
    done

    lemma divAlg_type: "[|a ∈ int;  b ∈ int|] ==> divAlg(<a,b>) ∈ int * int"
    apply (auto simp add: divAlg_def)
    apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type)
    done

    (** intify cancellation **)

    lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
    apply (simp (no_asm) add: zdiv_def)
    done

    lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
    apply (simp (no_asm) add: zdiv_def)
    done

    lemma zdiv_type [iff,TC]: "z zdiv w ∈ int"
    apply (unfold zdiv_def)
    apply (blast intro: fst_type divAlg_type)
    done

    lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
    apply (simp (no_asm) add: zmod_def)
    done

    lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
    apply (simp (no_asm) add: zmod_def)
    done

    lemma zmod_type [iff,TC]: "z zmod w ∈ int"
    apply (unfold zmod_def)
    apply (rule snd_type)
    apply (blast intro: divAlg_type)
    done

    (** Arbitrary definitions for division by zero.  Useful to simplify
        certain equations **)

    lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
    apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor)
    done  (*NOT for adding to default simpset*)

    lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
    apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor)
    done  (*NOT for adding to default simpset*)

    (** Basic laws about division and remainder **)

    lemma raw_zmod_zdiv_equality:
         "[| a ∈ int; b ∈ int |] ==> a = b $* (a zdiv b) $+ (a zmod b)"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (cut_tac a = "a" and b = "b" in divAlg_correct)
    apply (auto simp add: quorem_def zdiv_def zmod_def split_def)
    done

    lemma zmod_zdiv_equality: "intify(a) = b $* (a zdiv b) $+ (a zmod b)"
    apply (rule trans)
    apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality)
    apply auto
    done

    lemma pos_mod: "#0 $< b ==> #0 $<= a zmod b & a zmod b $< b"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
    apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
    apply (blast dest: zle_zless_trans)+
    done

    lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard]
    and    pos_mod_bound = pos_mod [THEN conjunct2, standard]

    lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
    apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
    apply (blast dest: zle_zless_trans)
    apply (blast dest: zless_trans)+
    done

    lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard]
    and    neg_mod_bound = neg_mod [THEN conjunct2, standard]

    (** proving general properties of zdiv and zmod **)

    lemma quorem_div_mod:
         "[|b ≠ #0;  a ∈ int;  b ∈ int |]
          ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
    apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
    apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
                          neg_mod_sign neg_mod_bound)
    done

    (*Surely quorem(<a,b>,<q,r>) implies a ∈ int, but it doesn't matter*)
    lemma quorem_div:
         "[| quorem(<a,b>,<q,r>);  b ≠ #0;  a ∈ int;  b ∈ int;  q ∈ int |]
          ==> a zdiv b = q"
    by (blast intro: quorem_div_mod [THEN unique_quotient])

    lemma quorem_mod:
         "[| quorem(<a,b>,<q,r>); b ≠ #0; a ∈ int; b ∈ int; q ∈ int; r ∈ int |]
          ==> a zmod b = r"
    by (blast intro: quorem_div_mod [THEN unique_remainder])

    lemma zdiv_pos_pos_trivial_raw:
         "[| a ∈ int;  b ∈ int;  #0 $<= a;  a $< b |] ==> a zdiv b = #0"
    apply (rule quorem_div)
    apply (auto simp add: quorem_def)
    (*linear arithmetic*)
    apply (blast dest: zle_zless_trans)+
    done

    lemma zdiv_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zdiv b = #0"
    apply (cut_tac a = "intify (a)" and b = "intify (b)"
           in zdiv_pos_pos_trivial_raw)
    apply auto
    done

    lemma zdiv_neg_neg_trivial_raw:
         "[| a ∈ int;  b ∈ int;  a $<= #0;  b $< a |] ==> a zdiv b = #0"
    apply (rule_tac r = "a" in quorem_div)
    apply (auto simp add: quorem_def)
    (*linear arithmetic*)
    apply (blast dest: zle_zless_trans zless_trans)+
    done

    lemma zdiv_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zdiv b = #0"
    apply (cut_tac a = "intify (a)" and b = "intify (b)"
           in zdiv_neg_neg_trivial_raw)
    apply auto
    done

    lemma zadd_le_0_lemma: "[| a$+b $<= #0;  #0 $< a;  #0 $< b |] ==> False"
    apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono)
    apply (auto simp add: zle_def)
    apply (blast dest: zless_trans)
    done

    lemma zdiv_pos_neg_trivial_raw:
         "[| a ∈ int;  b ∈ int;  #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
    apply (rule_tac r = "a $+ b" in quorem_div)
    apply (auto simp add: quorem_def)
    (*linear arithmetic*)
    apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
    done

    lemma zdiv_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
    apply (cut_tac a = "intify (a)" and b = "intify (b)"
           in zdiv_pos_neg_trivial_raw)
    apply auto
    done

    (*There is no zdiv_neg_pos_trivial because  #0 zdiv b = #0 would supersede it*)

    lemma zmod_pos_pos_trivial_raw:
         "[| a ∈ int;  b ∈ int;  #0 $<= a;  a $< b |] ==> a zmod b = a"
    apply (rule_tac q = "#0" in quorem_mod)
    apply (auto simp add: quorem_def)
    (*linear arithmetic*)
    apply (blast dest: zle_zless_trans)+
    done

    lemma zmod_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zmod b = intify(a)"
    apply (cut_tac a = "intify (a)" and b = "intify (b)"
           in zmod_pos_pos_trivial_raw)
    apply auto
    done

    lemma zmod_neg_neg_trivial_raw:
         "[| a ∈ int;  b ∈ int;  a $<= #0;  b $< a |] ==> a zmod b = a"
    apply (rule_tac q = "#0" in quorem_mod)
    apply (auto simp add: quorem_def)
    (*linear arithmetic*)
    apply (blast dest: zle_zless_trans zless_trans)+
    done

    lemma zmod_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zmod b = intify(a)"
    apply (cut_tac a = "intify (a)" and b = "intify (b)"
           in zmod_neg_neg_trivial_raw)
    apply auto
    done

    lemma zmod_pos_neg_trivial_raw:
         "[| a ∈ int;  b ∈ int;  #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
    apply (rule_tac q = "#-1" in quorem_mod)
    apply (auto simp add: quorem_def)
    (*linear arithmetic*)
    apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
    done

    lemma zmod_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
    apply (cut_tac a = "intify (a)" and b = "intify (b)"
           in zmod_pos_neg_trivial_raw)
    apply auto
    done

    (*There is no zmod_neg_pos_trivial...*)

    (*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*)

    lemma zdiv_zminus_zminus_raw:
         "[|a ∈ int;  b ∈ int|] ==> ($-a) zdiv ($-b) = a zdiv b"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div])
    apply auto
    done

    lemma zdiv_zminus_zminus [simp]: "($-a) zdiv ($-b) = a zdiv b"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw)
    apply auto
    done

    (*Simpler laws such as -a zmod b = -(a zmod b) FAIL*)
    lemma zmod_zminus_zminus_raw:
         "[|a ∈ int;  b ∈ int|] ==> ($-a) zmod ($-b) = $- (a zmod b)"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod])
    apply auto
    done

    lemma zmod_zminus_zminus [simp]: "($-a) zmod ($-b) = $- (a zmod b)"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw)
    apply auto
    done

    subsection{* division of a number by itself *}

    lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
    apply (subgoal_tac "#0 $< a$*q")
    apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
    apply (simp add: int_0_less_mult_iff)
    apply (blast dest: zless_trans)
    (*linear arithmetic...*)
    apply (drule_tac t = "%x. x $- r" in subst_context)
    apply (drule sym)
    apply (simp add: zcompare_rls)
    done

    lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
    apply (subgoal_tac "#0 $<= a$* (#1$-q)")
     apply (simp add: int_0_le_mult_iff zcompare_rls)
     apply (blast dest: zle_zless_trans)
    apply (simp add: zdiff_zmult_distrib2)
    apply (drule_tac t = "%x. x $- a $* q" in subst_context)
    apply (simp add: zcompare_rls)
    done

    lemma self_quotient:
         "[| quorem(<a,a>,<q,r>);  a ∈ int;  q ∈ int;  a ≠ #0|] ==> q = #1"
    apply (simp add: split_ifs quorem_def neq_iff_zless)
    apply (rule zle_anti_sym)
    apply safe
    apply auto
    prefer 4 apply (blast dest: zless_trans)
    apply (blast dest: zless_trans)
    apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1)
    apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2)
    apply (rule_tac [6] zminus_equation [THEN iffD1])
    apply (rule_tac [2] zminus_equation [THEN iffD1])
    apply (force intro: self_quotient_aux1 self_quotient_aux2
      simp add: zadd_commute zmult_zminus)+
    done

    lemma self_remainder:
         "[|quorem(<a,a>,<q,r>); a ∈ int; q ∈ int; r ∈ int; a ≠ #0|] ==> r = #0"
    apply (frule self_quotient)
    apply (auto simp add: quorem_def)
    done

    lemma zdiv_self_raw: "[|a ≠ #0; a ∈ int|] ==> a zdiv a = #1"
    apply (blast intro: quorem_div_mod [THEN self_quotient])
    done

    lemma zdiv_self [simp]: "intify(a) ≠ #0 ==> a zdiv a = #1"
    apply (drule zdiv_self_raw)
    apply auto
    done

    (*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *)
    lemma zmod_self_raw: "a ∈ int ==> a zmod a = #0"
    apply (case_tac "a = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (blast intro: quorem_div_mod [THEN self_remainder])
    done

    lemma zmod_self [simp]: "a zmod a = #0"
    apply (cut_tac a = "intify (a)" in zmod_self_raw)
    apply auto
    done

    subsection{* Computation of division and remainder *}

    lemma zdiv_zero [simp]: "#0 zdiv b = #0"
    apply (simp (no_asm) add: zdiv_def divAlg_def)
    done

    lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
    apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
    done

    lemma zmod_zero [simp]: "#0 zmod b = #0"
    apply (simp (no_asm) add: zmod_def divAlg_def)
    done

    lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
    apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
    done

    lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1"
    apply (simp (no_asm_simp) add: zmod_def divAlg_def)
    done

    (** a positive, b positive **)

    lemma zdiv_pos_pos: "[| #0 $< a;  #0 $<= b |]
          ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
    apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
    apply (auto simp add: zle_def)
    done

    lemma zmod_pos_pos:
         "[| #0 $< a;  #0 $<= b |]
          ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
    apply (simp (no_asm_simp) add: zmod_def divAlg_def)
    apply (auto simp add: zle_def)
    done

    (** a negative, b positive **)

    lemma zdiv_neg_pos:
         "[| a $< #0;  #0 $< b |]
          ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))"
    apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
    apply (blast dest: zle_zless_trans)
    done

    lemma zmod_neg_pos:
         "[| a $< #0;  #0 $< b |]
          ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))"
    apply (simp (no_asm_simp) add: zmod_def divAlg_def)
    apply (blast dest: zle_zless_trans)
    done

    (** a positive, b negative **)

    lemma zdiv_pos_neg:
         "[| #0 $< a;  b $< #0 |]
          ==> a zdiv b = fst (negateSnd(negDivAlg (<$-a, $-b>)))"
    apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle)
    apply auto
    apply (blast dest: zle_zless_trans)+
    apply (blast dest: zless_trans)
    apply (blast intro: zless_imp_zle)
    done

    lemma zmod_pos_neg:
         "[| #0 $< a;  b $< #0 |]
          ==> a zmod b = snd (negateSnd(negDivAlg (<$-a, $-b>)))"
    apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle)
    apply auto
    apply (blast dest: zle_zless_trans)+
    apply (blast dest: zless_trans)
    apply (blast intro: zless_imp_zle)
    done

    (** a negative, b negative **)

    lemma zdiv_neg_neg:
         "[| a $< #0;  b $<= #0 |]
          ==> a zdiv b = fst (negateSnd(posDivAlg(<$-a, $-b>)))"
    apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
    apply auto
    apply (blast dest!: zle_zless_trans)+
    done

    lemma zmod_neg_neg:
         "[| a $< #0;  b $<= #0 |]
          ==> a zmod b = snd (negateSnd(posDivAlg(<$-a, $-b>)))"
    apply (simp (no_asm_simp) add: zmod_def divAlg_def)
    apply auto
    apply (blast dest!: zle_zless_trans)+
    done

    declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
    declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
    declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]

    (** Special-case simplification **)

    lemma zmod_1 [simp]: "a zmod #1 = #0"
    apply (cut_tac a = "a" and b = "#1" in pos_mod_sign)
    apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound)
    apply auto
    (*arithmetic*)
    apply (drule add1_zle_iff [THEN iffD2])
    apply (rule zle_anti_sym)
    apply auto
    done

    lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)"
    apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality)
    apply auto
    done

    lemma zmod_minus1_right [simp]: "a zmod #-1 = #0"
    apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign)
    apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound)
    apply auto
    (*arithmetic*)
    apply (drule add1_zle_iff [THEN iffD2])
    apply (rule zle_anti_sym)
    apply auto
    done

    lemma zdiv_minus1_right_raw: "a ∈ int ==> a zdiv #-1 = $-a"
    apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality)
    apply auto
    apply (rule equation_zminus [THEN iffD2])
    apply auto
    done

    lemma zdiv_minus1_right: "a zdiv #-1 = $-a"
    apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw)
    apply auto
    done
    declare zdiv_minus1_right [simp]

    subsection{* Monotonicity in the first argument (divisor) *}

    lemma zdiv_mono1: "[| a $<= a';  #0 $< b |] ==> a zdiv b $<= a' zdiv b"
    apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
    apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
    apply (rule unique_quotient_lemma)
    apply (erule subst)
    apply (erule subst)
    apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound)
    done

    lemma zdiv_mono1_neg: "[| a $<= a';  b $< #0 |] ==> a' zdiv b $<= a zdiv b"
    apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
    apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
    apply (rule unique_quotient_lemma_neg)
    apply (erule subst)
    apply (erule subst)
    apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound)
    done

    subsection{* Monotonicity in the second argument (dividend) *}

    lemma q_pos_lemma:
         "[| #0 $<= b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $<= q'"
    apply (subgoal_tac "#0 $< b'$* (q' $+ #1)")
     apply (simp add: int_0_less_mult_iff)
     apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1])
    apply (simp add: zadd_zmult_distrib2)
    apply (erule zle_zless_trans)
    apply (erule zadd_zless_mono2)
    done

    lemma zdiv_mono2_lemma:
         "[| b$*q $+ r = b'$*q' $+ r';  #0 $<= b'$*q' $+ r';
             r' $< b';  #0 $<= r;  #0 $< b';  b' $<= b |]
          ==> q $<= q'"
    apply (frule q_pos_lemma, assumption+)
    apply (subgoal_tac "b$*q $< b$* (q' $+ #1)")
     apply (simp add: zmult_zless_cancel1)
     apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans)
    apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'")
     prefer 2 apply (simp add: zcompare_rls)
    apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
    apply (subst zadd_commute [of "b $× q'"], rule zadd_zless_mono)
     prefer 2 apply (blast intro: zmult_zle_mono1)
    apply (subgoal_tac "r' $+ #0 $< b $+ r")
     apply (simp add: zcompare_rls)
    apply (rule zadd_zless_mono)
     apply auto
    apply (blast dest: zless_zle_trans)
    done

    lemma zdiv_mono2_raw:
         "[| #0 $<= a;  #0 $< b';  b' $<= b;  a ∈ int |]
          ==> a zdiv b $<= a zdiv b'"
    apply (subgoal_tac "#0 $< b")
     prefer 2 apply (blast dest: zless_zle_trans)
    apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
    apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
    apply (rule zdiv_mono2_lemma)
    apply (erule subst)
    apply (erule subst)
    apply (simp_all add: pos_mod_sign pos_mod_bound)
    done

    lemma zdiv_mono2:
         "[| #0 $<= a;  #0 $< b';  b' $<= b |]
          ==> a zdiv b $<= a zdiv b'"
    apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
    apply auto
    done

    lemma q_neg_lemma:
         "[| b'$*q' $+ r' $< #0;  #0 $<= r';  #0 $< b' |] ==> q' $< #0"
    apply (subgoal_tac "b'$*q' $< #0")
     prefer 2 apply (force intro: zle_zless_trans)
    apply (simp add: zmult_less_0_iff)
    apply (blast dest: zless_trans)
    done

    lemma zdiv_mono2_neg_lemma:
         "[| b$*q $+ r = b'$*q' $+ r';  b'$*q' $+ r' $< #0;
             r $< b;  #0 $<= r';  #0 $< b';  b' $<= b |]
          ==> q' $<= q"
    apply (subgoal_tac "#0 $< b")
     prefer 2 apply (blast dest: zless_zle_trans)
    apply (frule q_neg_lemma, assumption+)
    apply (subgoal_tac "b$*q' $< b$* (q $+ #1)")
     apply (simp add: zmult_zless_cancel1)
     apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
    apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
    apply (subgoal_tac "b$*q' $<= b'$*q'")
     prefer 2
     apply (simp add: zmult_zle_cancel2)
     apply (blast dest: zless_trans)
    apply (subgoal_tac "b'$*q' $+ r $< b $+ (b$*q $+ r)")
     prefer 2
     apply (erule ssubst)
     apply simp
     apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono)
      apply (assumption)
     apply simp
    apply (simp (no_asm_use) add: zadd_commute)
    apply (rule zle_zless_trans)
     prefer 2 apply (assumption)
    apply (simp (no_asm_simp) add: zmult_zle_cancel2)
    apply (blast dest: zless_trans)
    done

    lemma zdiv_mono2_neg_raw:
         "[| a $< #0;  #0 $< b';  b' $<= b;  a ∈ int |]
          ==> a zdiv b' $<= a zdiv b"
    apply (subgoal_tac "#0 $< b")
     prefer 2 apply (blast dest: zless_zle_trans)
    apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
    apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
    apply (rule zdiv_mono2_neg_lemma)
    apply (erule subst)
    apply (erule subst)
    apply (simp_all add: pos_mod_sign pos_mod_bound)
    done

    lemma zdiv_mono2_neg: "[| a $< #0;  #0 $< b';  b' $<= b |]
          ==> a zdiv b' $<= a zdiv b"
    apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
    apply auto
    done

    subsection{* More algebraic laws for zdiv and zmod *}

    (** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **)

    lemma zmult1_lemma:
         "[| quorem(<b,c>, <q,r>);  c ∈ int;  c ≠ #0 |]
          ==> quorem (<a$*b, c>, <a$*q $+ (a$*r) zdiv c, (a$*r) zmod c>)"
    apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
                          pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
    apply (auto intro: raw_zmod_zdiv_equality)
    done

    lemma zdiv_zmult1_eq_raw:
         "[|b ∈ int;  c ∈ int|]
          ==> (a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
    apply (case_tac "c = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
    apply auto
    done

    lemma zdiv_zmult1_eq: "(a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
    apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw)
    apply auto
    done

    lemma zmod_zmult1_eq_raw:
         "[|b ∈ int;  c ∈ int|] ==> (a$*b) zmod c = a$*(b zmod c) zmod c"
    apply (case_tac "c = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
    apply auto
    done

    lemma zmod_zmult1_eq: "(a$*b) zmod c = a$*(b zmod c) zmod c"
    apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw)
    apply auto
    done

    lemma zmod_zmult1_eq': "(a$*b) zmod c = ((a zmod c) $* b) zmod c"
    apply (rule trans)
    apply (rule_tac b = " (b $* a) zmod c" in trans)
    apply (rule_tac [2] zmod_zmult1_eq)
    apply (simp_all (no_asm) add: zmult_commute)
    done

    lemma zmod_zmult_distrib: "(a$*b) zmod c = ((a zmod c) $* (b zmod c)) zmod c"
    apply (rule zmod_zmult1_eq' [THEN trans])
    apply (rule zmod_zmult1_eq)
    done

    lemma zdiv_zmult_self1 [simp]: "intify(b) ≠ #0 ==> (a$*b) zdiv b = intify(a)"
    apply (simp (no_asm_simp) add: zdiv_zmult1_eq)
    done

    lemma zdiv_zmult_self2 [simp]: "intify(b) ≠ #0 ==> (b$*a) zdiv b = intify(a)"
    apply (subst zmult_commute , erule zdiv_zmult_self1)
    done

    lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0"
    apply (simp (no_asm) add: zmod_zmult1_eq)
    done

    lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0"
    apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq)
    done

    (** proving (a$+b) zdiv c =
                a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **)

    lemma zadd1_lemma:
         "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
             c ∈ int;  c ≠ #0 |]
          ==> quorem (<a$+b, c>, <aq $+ bq $+ (ar$+br) zdiv c, (ar$+br) zmod c>)"
    apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
                          pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
    apply (auto intro: raw_zmod_zdiv_equality)
    done

    (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    lemma zdiv_zadd1_eq_raw:
         "[|a ∈ int; b ∈ int; c ∈ int|] ==>
          (a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
    apply (case_tac "c = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
                                     THEN quorem_div])
    done

    lemma zdiv_zadd1_eq:
         "(a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
           in zdiv_zadd1_eq_raw)
    apply auto
    done

    lemma zmod_zadd1_eq_raw:
         "[|a ∈ int; b ∈ int; c ∈ int|]
          ==> (a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
    apply (case_tac "c = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
                                     THEN quorem_mod])
    done

    lemma zmod_zadd1_eq: "(a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
           in zmod_zadd1_eq_raw)
    apply auto
    done

    lemma zmod_div_trivial_raw:
         "[|a ∈ int; b ∈ int|] ==> (a zmod b) zdiv b = #0"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
             zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial)
    done

    lemma zmod_div_trivial [simp]: "(a zmod b) zdiv b = #0"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_div_trivial_raw)
    apply auto
    done

    lemma zmod_mod_trivial_raw:
         "[|a ∈ int; b ∈ int|] ==> (a zmod b) zmod b = a zmod b"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
           zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial)
    done

    lemma zmod_mod_trivial [simp]: "(a zmod b) zmod b = a zmod b"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_mod_trivial_raw)
    apply auto
    done

    lemma zmod_zadd_left_eq: "(a$+b) zmod c = ((a zmod c) $+ b) zmod c"
    apply (rule trans [symmetric])
    apply (rule zmod_zadd1_eq)
    apply (simp (no_asm))
    apply (rule zmod_zadd1_eq [symmetric])
    done

    lemma zmod_zadd_right_eq: "(a$+b) zmod c = (a $+ (b zmod c)) zmod c"
    apply (rule trans [symmetric])
    apply (rule zmod_zadd1_eq)
    apply (simp (no_asm))
    apply (rule zmod_zadd1_eq [symmetric])
    done

    lemma zdiv_zadd_self1 [simp]:
         "intify(a) ≠ #0 ==> (a$+b) zdiv a = b zdiv a $+ #1"
    by (simp (no_asm_simp) add: zdiv_zadd1_eq)

    lemma zdiv_zadd_self2 [simp]:
         "intify(a) ≠ #0 ==> (b$+a) zdiv a = b zdiv a $+ #1"
    by (simp (no_asm_simp) add: zdiv_zadd1_eq)

    lemma zmod_zadd_self1 [simp]: "(a$+b) zmod a = b zmod a"
    apply (case_tac "a = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (simp (no_asm_simp) add: zmod_zadd1_eq)
    done

    lemma zmod_zadd_self2 [simp]: "(b$+a) zmod a = b zmod a"
    apply (case_tac "a = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (simp (no_asm_simp) add: zmod_zadd1_eq)
    done

    subsection{* proving  a zdiv (b*c) = (a zdiv b) zdiv c *}

    (*The condition c>0 seems necessary.  Consider that 7 zdiv ~6 = ~2 but
      7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1.  The subcase (a zdiv b) zmod c = 0 seems
      to cause particular problems.*)

    (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)

    lemma zdiv_zmult2_aux1:
         "[| #0 $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
    apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1")
    apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
    apply (rule zle_zless_trans)
    apply (erule_tac [2] zmult_zless_mono1)
    apply (rule zmult_zle_mono2_neg)
    apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
    apply (blast intro: zless_imp_zle dest: zless_zle_trans)
    done

    lemma zdiv_zmult2_aux2:
         "[| #0 $< c;   b $< r;  r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0"
    apply (subgoal_tac "b $* (q zmod c) $<= #0")
     prefer 2
     apply (simp add: zmult_le_0_iff pos_mod_sign)
     apply (blast intro: zless_imp_zle dest: zless_zle_trans)
    (*arithmetic*)
    apply (drule zadd_zle_mono)
    apply assumption
    apply (simp add: zadd_commute)
    done

    lemma zdiv_zmult2_aux3:
         "[| #0 $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q zmod c) $+ r"
    apply (subgoal_tac "#0 $<= b $* (q zmod c)")
     prefer 2
     apply (simp add: int_0_le_mult_iff pos_mod_sign)
     apply (blast intro: zless_imp_zle dest: zle_zless_trans)
    (*arithmetic*)
    apply (drule zadd_zle_mono)
    apply assumption
    apply (simp add: zadd_commute)
    done

    lemma zdiv_zmult2_aux4:
         "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
    apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)")
    apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
    apply (rule zless_zle_trans)
    apply (erule zmult_zless_mono1)
    apply (rule_tac [2] zmult_zle_mono2)
    apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
    apply (blast intro: zless_imp_zle dest: zle_zless_trans)
    done

    lemma zdiv_zmult2_lemma:
         "[| quorem (<a,b>, <q,r>);  a ∈ int;  b ∈ int;  b ≠ #0;  #0 $< c |]
          ==> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)"
    apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
                   neq_iff_zless int_0_less_mult_iff
                   zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
                   zdiv_zmult2_aux3 zdiv_zmult2_aux4)
    apply (blast dest: zless_trans)+
    done

    lemma zdiv_zmult2_eq_raw:
         "[|#0 $< c;  a ∈ int;  b ∈ int|] ==> a zdiv (b$*c) = (a zdiv b) zdiv c"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div])
    apply (auto simp add: intify_eq_0_iff_zle)
    apply (blast dest: zle_zless_trans)
    done

    lemma zdiv_zmult2_eq: "#0 $< c ==> a zdiv (b$*c) = (a zdiv b) zdiv c"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zmult2_eq_raw)
    apply auto
    done

    lemma zmod_zmult2_eq_raw:
         "[|#0 $< c;  a ∈ int;  b ∈ int|]
          ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod])
    apply (auto simp add: intify_eq_0_iff_zle)
    apply (blast dest: zle_zless_trans)
    done

    lemma zmod_zmult2_eq:
         "#0 $< c ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
    apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw)
    apply auto
    done

    subsection{* Cancellation of common factors in "zdiv" *}

    lemma zdiv_zmult_zmult1_aux1:
         "[| #0 $< b;  intify(c) ≠ #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
    apply (subst zdiv_zmult2_eq)
    apply auto
    done

    lemma zdiv_zmult_zmult1_aux2:
         "[| b $< #0;  intify(c) ≠ #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
    apply (subgoal_tac " (c $* ($-a)) zdiv (c $* ($-b)) = ($-a) zdiv ($-b)")
    apply (rule_tac [2] zdiv_zmult_zmult1_aux1)
    apply auto
    done

    lemma zdiv_zmult_zmult1_raw:
         "[|intify(c) ≠ #0; b ∈ int|] ==> (c$*a) zdiv (c$*b) = a zdiv b"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (auto simp add: neq_iff_zless [of b]
      zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
    done

    lemma zdiv_zmult_zmult1: "intify(c) ≠ #0 ==> (c$*a) zdiv (c$*b) = a zdiv b"
    apply (cut_tac b = "intify (b)" in zdiv_zmult_zmult1_raw)
    apply auto
    done

    lemma zdiv_zmult_zmult2: "intify(c) ≠ #0 ==> (a$*c) zdiv (b$*c) = a zdiv b"
    apply (drule zdiv_zmult_zmult1)
    apply (auto simp add: zmult_commute)
    done

    subsection{* Distribution of factors over "zmod" *}

    lemma zmod_zmult_zmult1_aux1:
         "[| #0 $< b;  intify(c) ≠ #0 |]
          ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
    apply (subst zmod_zmult2_eq)
    apply auto
    done

    lemma zmod_zmult_zmult1_aux2:
         "[| b $< #0;  intify(c) ≠ #0 |]
          ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
    apply (subgoal_tac " (c $* ($-a)) zmod (c $* ($-b)) = c $* (($-a) zmod ($-b))")
    apply (rule_tac [2] zmod_zmult_zmult1_aux1)
    apply auto
    done

    lemma zmod_zmult_zmult1_raw:
         "[|b ∈ int; c ∈ int|] ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
    apply (case_tac "b = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (case_tac "c = #0")
     apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
    apply (auto simp add: neq_iff_zless [of b]
      zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
    done

    lemma zmod_zmult_zmult1: "(c$*a) zmod (c$*b) = c $* (a zmod b)"
    apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult_zmult1_raw)
    apply auto
    done

    lemma zmod_zmult_zmult2: "(a$*c) zmod (b$*c) = (a zmod b) $* c"
    apply (cut_tac c = "c" in zmod_zmult_zmult1)
    apply (auto simp add: zmult_commute)
    done

    (** Quotients of signs **)

    lemma zdiv_neg_pos_less0: "[| a $< #0;  #0 $< b |] ==> a zdiv b $< #0"
    apply (subgoal_tac "a zdiv b $<= #-1")
    apply (erule zle_zless_trans)
    apply (simp (no_asm))
    apply (rule zle_trans)
    apply (rule_tac a' = "#-1" in zdiv_mono1)
    apply (rule zless_add1_iff_zle [THEN iffD1])
    apply (simp (no_asm))
    apply (auto simp add: zdiv_minus1)
    done

    lemma zdiv_nonneg_neg_le0: "[| #0 $<= a;  b $< #0 |] ==> a zdiv b $<= #0"
    apply (drule zdiv_mono1_neg)
    apply auto
    done

    lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)"
    apply auto
    apply (drule_tac [2] zdiv_mono1)
    apply (auto simp add: neq_iff_zless)
    apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym])
    apply (blast intro: zdiv_neg_pos_less0)
    done

    lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)"
    apply (subst zdiv_zminus_zminus [symmetric])
    apply (rule iff_trans)
    apply (rule pos_imp_zdiv_nonneg_iff)
    apply auto
    done

    (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
    lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)"
    apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
    apply (erule pos_imp_zdiv_nonneg_iff)
    done

    (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
    lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)"
    apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
    apply (erule neg_imp_zdiv_nonneg_iff)
    done

    (*
     THESE REMAIN TO BE CONVERTED -- but aren't that useful!

     subsection{* Speeding up the division algorithm with shifting *}

     (** computing "zdiv" by shifting **)

     lemma pos_zdiv_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zdiv (#2$*a) = b zdiv a"
     apply (case_tac "a = #0")
     apply (subgoal_tac "#1 $<= a")
      apply (arith_tac 2)
     apply (subgoal_tac "#1 $< a $* #2")
      apply (arith_tac 2)
     apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
      apply (rule_tac [2] zmult_zle_mono2)
     apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
     apply (subst zdiv_zadd1_eq)
     apply (simp (no_asm_simp) add: zdiv_zmult_zmult2 zmod_zmult_zmult2 zdiv_pos_pos_trivial)
     apply (subst zdiv_pos_pos_trivial)
     apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
     apply (auto simp add: zmod_pos_pos_trivial)
     apply (subgoal_tac "#0 $<= b zmod a")
      apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
     apply arith
     done

     lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) <-> (b$+#1) zdiv a"
     apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) <-> ($-b-#1) zdiv ($-a)")
     apply (rule_tac [2] pos_zdiv_mult_2)
     apply (auto simp add: zmult_zminus_right)
     apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
     apply (Simp_tac 2)
     apply (asm_full_simp_tac (HOL_ss add: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
     done

     (*Not clear why this must be proved separately; probably integ_of causes
       simplification problems*)
     lemma lemma: "~ #0 $<= x ==> x $<= #0"
     apply auto
     done

     lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =
               (if ~b | #0 $<= integ_of w
                then integ_of v zdiv (integ_of w)
                else (integ_of v $+ #1) zdiv (integ_of w))"
     apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
     apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2)
     done

     declare zdiv_integ_of_BIT [simp]

     (** computing "zmod" by shifting (proofs resemble those for "zdiv") **)

     lemma pos_zmod_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zmod (#2$*a) = #1 $+ #2 $* (b zmod a)"
     apply (case_tac "a = #0")
     apply (subgoal_tac "#1 $<= a")
      apply (arith_tac 2)
     apply (subgoal_tac "#1 $< a $* #2")
      apply (arith_tac 2)
     apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
      apply (rule_tac [2] zmult_zle_mono2)
     apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
     apply (subst zmod_zadd1_eq)
     apply (simp (no_asm_simp) add: zmod_zmult_zmult2 zmod_pos_pos_trivial)
     apply (rule zmod_pos_pos_trivial)
     apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
     apply (auto simp add: zmod_pos_pos_trivial)
     apply (subgoal_tac "#0 $<= b zmod a")
      apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
     apply arith
     done

     lemma neg_zmod_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zmod (#2$*a) = #2 $* ((b$+#1) zmod a) - #1"
     apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zmod (#2$* ($-a)) = #1 $+ #2$* (($-b-#1) zmod ($-a))")
     apply (rule_tac [2] pos_zmod_mult_2)
     apply (auto simp add: zmult_zminus_right)
     apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
     apply (Simp_tac 2)
     apply (asm_full_simp_tac (HOL_ss add: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
     apply (dtac (zminus_equation [THEN iffD1, symmetric])
     apply auto
     done

     lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =
               (if b then
                     if #0 $<= integ_of w
                     then #2 $* (integ_of v zmod integ_of w) $+ #1
                     else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1
                else #2 $* (integ_of v zmod integ_of w))"
     apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
     apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2)
     done

     declare zmod_integ_of_BIT [simp]
    *)

    ML{*
    val zspos_add_zspos_imp_zspos = thm "zspos_add_zspos_imp_zspos";
    val zpos_add_zpos_imp_zpos = thm "zpos_add_zpos_imp_zpos";
    val zneg_add_zneg_imp_zneg = thm "zneg_add_zneg_imp_zneg";
    val zneg_or_0_add_zneg_or_0_imp_zneg_or_0 = thm "zneg_or_0_add_zneg_or_0_imp_zneg_or_0";
    val zero_lt_zmagnitude = thm "zero_lt_zmagnitude";
    val zless_add_succ_iff = thm "zless_add_succ_iff";
    val zadd_succ_zle_iff = thm "zadd_succ_zle_iff";
    val zless_add1_iff_zle = thm "zless_add1_iff_zle";
    val add1_zle_iff = thm "add1_zle_iff";
    val add1_left_zle_iff = thm "add1_left_zle_iff";
    val zmult_zle_mono1 = thm "zmult_zle_mono1";
    val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
    val zmult_zle_mono2 = thm "zmult_zle_mono2";
    val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
    val zmult_zle_mono = thm "zmult_zle_mono";
    val zmult_zless_mono2 = thm "zmult_zless_mono2";
    val zmult_zless_mono1 = thm "zmult_zless_mono1";
    val zmult_zless_mono = thm "zmult_zless_mono";
    val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
    val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
    val zmult_eq_0_iff = thm "zmult_eq_0_iff";
    val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
    val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
    val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
    val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
    val int_eq_iff_zle = thm "int_eq_iff_zle";
    val zmult_cancel2 = thm "zmult_cancel2";
    val zmult_cancel1 = thm "zmult_cancel1";
    val unique_quotient = thm "unique_quotient";
    val unique_remainder = thm "unique_remainder";
    val adjust_eq = thm "adjust_eq";
    val posDivAlg_termination = thm "posDivAlg_termination";
    val posDivAlg_unfold = thm "posDivAlg_unfold";
    val posDivAlg_eqn = thm "posDivAlg_eqn";
    val posDivAlg_induct = thm "posDivAlg_induct";
    val intify_eq_0_iff_zle = thm "intify_eq_0_iff_zle";
    val zmult_pos = thm "zmult_pos";
    val zmult_neg = thm "zmult_neg";
    val zmult_pos_neg = thm "zmult_pos_neg";
    val int_0_less_mult_iff = thm "int_0_less_mult_iff";
    val int_0_le_mult_iff = thm "int_0_le_mult_iff";
    val zmult_less_0_iff = thm "zmult_less_0_iff";
    val zmult_le_0_iff = thm "zmult_le_0_iff";
    val posDivAlg_type = thm "posDivAlg_type";
    val posDivAlg_correct = thm "posDivAlg_correct";
    val negDivAlg_termination = thm "negDivAlg_termination";
    val negDivAlg_unfold = thm "negDivAlg_unfold";
    val negDivAlg_eqn = thm "negDivAlg_eqn";
    val negDivAlg_induct = thm "negDivAlg_induct";
    val negDivAlg_type = thm "negDivAlg_type";
    val negDivAlg_correct = thm "negDivAlg_correct";
    val quorem_0 = thm "quorem_0";
    val posDivAlg_zero_divisor = thm "posDivAlg_zero_divisor";
    val posDivAlg_0 = thm "posDivAlg_0";
    val negDivAlg_minus1 = thm "negDivAlg_minus1";
    val negateSnd_eq = thm "negateSnd_eq";
    val negateSnd_type = thm "negateSnd_type";
    val quorem_neg = thm "quorem_neg";
    val divAlg_correct = thm "divAlg_correct";
    val divAlg_type = thm "divAlg_type";
    val zdiv_intify1 = thm "zdiv_intify1";
    val zdiv_intify2 = thm "zdiv_intify2";
    val zdiv_type = thm "zdiv_type";
    val zmod_intify1 = thm "zmod_intify1";
    val zmod_intify2 = thm "zmod_intify2";
    val zmod_type = thm "zmod_type";
    val DIVISION_BY_ZERO_ZDIV = thm "DIVISION_BY_ZERO_ZDIV";
    val DIVISION_BY_ZERO_ZMOD = thm "DIVISION_BY_ZERO_ZMOD";
    val zmod_zdiv_equality = thm "zmod_zdiv_equality";
    val pos_mod = thm "pos_mod";
    val pos_mod_sign = thm "pos_mod_sign";
    val neg_mod = thm "neg_mod";
    val neg_mod_sign = thm "neg_mod_sign";
    val quorem_div_mod = thm "quorem_div_mod";
    val quorem_div = thm "quorem_div";
    val quorem_mod = thm "quorem_mod";
    val zdiv_pos_pos_trivial = thm "zdiv_pos_pos_trivial";
    val zdiv_neg_neg_trivial = thm "zdiv_neg_neg_trivial";
    val zdiv_pos_neg_trivial = thm "zdiv_pos_neg_trivial";
    val zmod_pos_pos_trivial = thm "zmod_pos_pos_trivial";
    val zmod_neg_neg_trivial = thm "zmod_neg_neg_trivial";
    val zmod_pos_neg_trivial = thm "zmod_pos_neg_trivial";
    val zdiv_zminus_zminus = thm "zdiv_zminus_zminus";
    val zmod_zminus_zminus = thm "zmod_zminus_zminus";
    val self_quotient = thm "self_quotient";
    val self_remainder = thm "self_remainder";
    val zdiv_self = thm "zdiv_self";
    val zmod_self = thm "zmod_self";
    val zdiv_zero = thm "zdiv_zero";
    val zdiv_eq_minus1 = thm "zdiv_eq_minus1";
    val zmod_zero = thm "zmod_zero";
    val zdiv_minus1 = thm "zdiv_minus1";
    val zmod_minus1 = thm "zmod_minus1";
    val zdiv_pos_pos = thm "zdiv_pos_pos";
    val zmod_pos_pos = thm "zmod_pos_pos";
    val zdiv_neg_pos = thm "zdiv_neg_pos";
    val zmod_neg_pos = thm "zmod_neg_pos";
    val zdiv_pos_neg = thm "zdiv_pos_neg";
    val zmod_pos_neg = thm "zmod_pos_neg";
    val zdiv_neg_neg = thm "zdiv_neg_neg";
    val zmod_neg_neg = thm "zmod_neg_neg";
    val zmod_1 = thm "zmod_1";
    val zdiv_1 = thm "zdiv_1";
    val zmod_minus1_right = thm "zmod_minus1_right";
    val zdiv_minus1_right = thm "zdiv_minus1_right";
    val zdiv_mono1 = thm "zdiv_mono1";
    val zdiv_mono1_neg = thm "zdiv_mono1_neg";
    val zdiv_mono2 = thm "zdiv_mono2";
    val zdiv_mono2_neg = thm "zdiv_mono2_neg";
    val zdiv_zmult1_eq = thm "zdiv_zmult1_eq";
    val zmod_zmult1_eq = thm "zmod_zmult1_eq";
    val zmod_zmult1_eq' = thm "zmod_zmult1_eq'";
    val zmod_zmult_distrib = thm "zmod_zmult_distrib";
    val zdiv_zmult_self1 = thm "zdiv_zmult_self1";
    val zdiv_zmult_self2 = thm "zdiv_zmult_self2";
    val zmod_zmult_self1 = thm "zmod_zmult_self1";
    val zmod_zmult_self2 = thm "zmod_zmult_self2";
    val zdiv_zadd1_eq = thm "zdiv_zadd1_eq";
    val zmod_zadd1_eq = thm "zmod_zadd1_eq";
    val zmod_div_trivial = thm "zmod_div_trivial";
    val zmod_mod_trivial = thm "zmod_mod_trivial";
    val zmod_zadd_left_eq = thm "zmod_zadd_left_eq";
    val zmod_zadd_right_eq = thm "zmod_zadd_right_eq";
    val zdiv_zadd_self1 = thm "zdiv_zadd_self1";
    val zdiv_zadd_self2 = thm "zdiv_zadd_self2";
    val zmod_zadd_self1 = thm "zmod_zadd_self1";
    val zmod_zadd_self2 = thm "zmod_zadd_self2";
    val zdiv_zmult2_eq = thm "zdiv_zmult2_eq";
    val zmod_zmult2_eq = thm "zmod_zmult2_eq";
    val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1";
    val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2";
    val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1";
    val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2";
    val zdiv_neg_pos_less0 = thm "zdiv_neg_pos_less0";
    val zdiv_nonneg_neg_le0 = thm "zdiv_nonneg_neg_le0";
    val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff";
    val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff";
    val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff";
    val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff";
    *}

    end

lemma zspos_add_zspos_imp_zspos:

      [| #0 $< x; #0 $< y |] ==> #0 $< x $+ y

lemma zpos_add_zpos_imp_zpos:

      [| #0 $≤ x; #0 $≤ y |] ==> #0 $≤ x $+ y

lemma zneg_add_zneg_imp_zneg:

      [| x $< #0; y $< #0 |] ==> x $+ y $< #0

lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:

      [| x $≤ #0; y $≤ #0 |] ==> x $+ y $≤ #0

lemma zero_lt_zmagnitude:

      [| #0 $< k; k ∈ int |] ==> 0 < zmagnitude(k)

lemma zless_add_succ_iff:

      w $< z $+ $# succ(m) <-> w $< z $+ $# m ∨ intify(w) = z $+ $# m

lemma zadd_succ_lemma:

      z ∈ int ==> w $+ $# succ(m) $≤ z <-> w $+ $# m $< z

lemma zadd_succ_zle_iff:

      w $+ $# succ(m) $≤ z <-> w $+ $# m $< z

lemma zless_add1_iff_zle:

      w $< z $+ #1 <-> w $≤ z

lemma add1_zle_iff:

      w $+ #1 $≤ z <-> w $< z

lemma add1_left_zle_iff:

      #1 $+ w $≤ z <-> w $< z

lemma zmult_mono_lemma:

      [| k ∈ nat; i $≤ j |] ==> i $× $# k $≤ j $× $# k

lemma zmult_zle_mono1:

      [| i $≤ j; #0 $≤ k |] ==> i $× k $≤ j $× k

lemma zmult_zle_mono1_neg:

      [| i $≤ j; k $≤ #0 |] ==> j $× k $≤ i $× k

lemma zmult_zle_mono2:

      [| i $≤ j; #0 $≤ k |] ==> k $× i $≤ k $× j

lemma zmult_zle_mono2_neg:

      [| i $≤ j; k $≤ #0 |] ==> k $× j $≤ k $× i

lemma zmult_zle_mono:

      [| i $≤ j; k $≤ l; #0 $≤ j; #0 $≤ k |] ==> i $× k $≤ j $× l

lemma zmult_zless_mono2_lemma:

      [| i $< j; k ∈ nat; 0 < k |] ==> $# k $× i $< $# k $× j

lemma zmult_zless_mono2:

      [| i $< j; #0 $< k |] ==> k $× i $< k $× j

lemma zmult_zless_mono1:

      [| i $< j; #0 $< k |] ==> i $× k $< j $× k

lemma zmult_zless_mono:

      [| i $< j; k $< l; #0 $< j; #0 $< k |] ==> i $× k $< j $× l

lemma zmult_zless_mono1_neg:

      [| i $< j; k $< #0 |] ==> j $× k $< i $× k

lemma zmult_zless_mono2_neg:

      [| i $< j; k $< #0 |] ==> k $× j $< k $× i

lemma zmult_eq_lemma:

      [| m ∈ int; n ∈ int |] ==> m = #0 ∨ n = #0 <-> m $× n = #0

lemma zmult_eq_0_iff:

      m $× n = #0 <-> intify(m) = #0 ∨ intify(n) = #0

lemma zmult_zless_lemma:

      [| k ∈ int; m ∈ int; n ∈ int |]
      ==> m $× k $< n $× k <-> #0 $< k ∧ m $< n ∨ k $< #0 ∧ n $< m

lemma zmult_zless_cancel2:

      m $× k $< n $× k <-> #0 $< k ∧ m $< n ∨ k $< #0 ∧ n $< m

lemma zmult_zless_cancel1:

      k $× m $< k $× n <-> #0 $< k ∧ m $< n ∨ k $< #0 ∧ n $< m

lemma zmult_zle_cancel2:

      m $× k $≤ n $× k <-> (#0 $< k --> m $≤ n) ∧ (k $< #0 --> n $≤ m)

lemma zmult_zle_cancel1:

      k $× m $≤ k $× n <-> (#0 $< k --> m $≤ n) ∧ (k $< #0 --> n $≤ m)

lemma int_eq_iff_zle:

      [| m ∈ int; n ∈ int |] ==> m = n <-> m $≤ n ∧ n $≤ m

lemma zmult_cancel2_lemma:

      [| k ∈ int; m ∈ int; n ∈ int |] ==> m $× k = n $× k <-> k = #0 ∨ m = n

lemma zmult_cancel2:

      m $× k = n $× k <-> intify(k) = #0 ∨ intify(m) = intify(n)

lemma zmult_cancel1:

      k $× m = k $× n <-> intify(k) = #0 ∨ intify(m) = intify(n)

### Uniqueness and monotonicity of quotients and remainders

lemma unique_quotient_lemma:

      [| b $× q' $+ r' $≤ b $× q $+ r; #0 $≤ r'; #0 $< b; r $< b |] ==> q' $≤ q

lemma unique_quotient_lemma_neg:

      [| b $× q' $+ r' $≤ b $× q $+ r; r $≤ #0; b $< #0; b $< r' |] ==> q $≤ q'

lemma unique_quotient:

      [| quorem(⟨a, b⟩, ⟨q, r⟩); quorem(⟨a, b⟩, ⟨q', r'⟩); b ∈ int; b ≠ #0; q ∈ int;
         q' ∈ int |]
      ==> q = q'

lemma unique_remainder:

      [| quorem(⟨a, b⟩, ⟨q, r⟩); quorem(⟨a, b⟩, ⟨q', r'⟩); b ∈ int; b ≠ #0; q ∈ int;
         q' ∈ int; r ∈ int; r' ∈ int |]
      ==> r = r'

### Correctness of posDivAlg, the Division Algorithm for @{text "a≥0"} and @{text "b>0"}

lemma adjust_eq:

      adjust(b, ⟨q, r⟩) =
      (let diff = r $- b
       in if #0 $≤ diff then ⟨#2 $× q $+ #1, diff⟩ else ⟨#2 $× q, r⟩)

lemma posDivAlg_termination:

      [| #0 $< b; ¬ a $< b |] ==> nat_of(a $- #2 $× b $+ #1) < nat_of(a $- b $+ #1)

lemmas posDivAlg_unfold:

      posDivAlg(a) =
      (%⟨a,b⟩ f. if a $< b ∨ b $≤ #0 then ⟨#0, a⟩ else adjust(b, f ` ⟨a, #2 $× b⟩))
       (a, λx∈measure(int × int, %⟨a,b⟩. nat_of(a $- b $+ #1)) -`` {a}. posDivAlg(x))

lemmas posDivAlg_unfold:

      posDivAlg(a) =
      (%⟨a,b⟩ f. if a $< b ∨ b $≤ #0 then ⟨#0, a⟩ else adjust(b, f ` ⟨a, #2 $× b⟩))
       (a, λx∈measure(int × int, %⟨a,b⟩. nat_of(a $- b $+ #1)) -`` {a}. posDivAlg(x))

lemma posDivAlg_eqn:

      [| #0 $< b; a ∈ int; b ∈ int |]
      ==> posDivAlg(⟨a, b⟩) =
          (if a $< b then ⟨#0, a⟩ else adjust(b, posDivAlg(⟨a, #2 $× b⟩)))

lemma posDivAlg_induct_lemma:

      (!!a b. [| a ∈ int; b ∈ int; ¬ (a $< b ∨ b $≤ #0) --> P(⟨a, #2 $× b⟩) |]
              ==> P(⟨a, b⟩))
      ==> ⟨u, v⟩ ∈ int × int --> P(⟨u, v⟩)

lemma posDivAlg_induct:

      [| u ∈ int; v ∈ int;
         !!a b. [| a ∈ int; b ∈ int; ¬ (a $< b ∨ b $≤ #0) --> P(a, #2 $× b) |]
                ==> P(a, b) |]
      ==> P(u, v)

lemma intify_eq_0_iff_zle:

      intify(m) = #0 <-> m $≤ #0 ∧ #0 $≤ m

### Some convenient biconditionals for products of signs

lemma zmult_pos:

      [| #0 $< i; #0 $< j |] ==> #0 $< i $× j

lemma zmult_neg:

      [| i $< #0; j $< #0 |] ==> #0 $< i $× j

lemma zmult_pos_neg:

      [| #0 $< i; j $< #0 |] ==> i $× j $< #0

lemma int_0_less_lemma:

      [| x ∈ int; y ∈ int |]
      ==> #0 $< x $× y <-> #0 $< x ∧ #0 $< y ∨ x $< #0 ∧ y $< #0

lemma int_0_less_mult_iff:

      #0 $< x $× y <-> #0 $< x ∧ #0 $< y ∨ x $< #0 ∧ y $< #0

lemma int_0_le_lemma:

      [| x ∈ int; y ∈ int |]
      ==> #0 $≤ x $× y <-> #0 $≤ x ∧ #0 $≤ y ∨ x $≤ #0 ∧ y $≤ #0

lemma int_0_le_mult_iff:

      #0 $≤ x $× y <-> #0 $≤ x ∧ #0 $≤ y ∨ x $≤ #0 ∧ y $≤ #0

lemma zmult_less_0_iff:

      x $× y $< #0 <-> #0 $< x ∧ y $< #0 ∨ x $< #0 ∧ #0 $< y

lemma zmult_le_0_iff:

      x $× y $≤ #0 <-> #0 $≤ x ∧ y $≤ #0 ∨ x $≤ #0 ∧ #0 $≤ y

lemma posDivAlg_type:

      [| a ∈ int; b ∈ int |] ==> posDivAlg(⟨a, b⟩) ∈ int × int

lemma posDivAlg_correct:

      [| a ∈ int; b ∈ int; #0 $≤ a; #0 $< b |] ==> quorem(⟨a, b⟩, posDivAlg(⟨a, b⟩))

### Correctness of negDivAlg, the division algorithm for a<0 and b>0

lemma negDivAlg_termination:

      [| #0 $< b; a $+ b $< #0 |] ==> nat_of($- a $- #2 $× b) < nat_of($- a $- b)

lemmas negDivAlg_unfold:

      negDivAlg(a) =
      (%⟨a,b⟩ f.
          if #0 $≤ a $+ b ∨ b $≤ #0 then ⟨#-1, a $+ b⟩
          else adjust(b, f ` ⟨a, #2 $× b⟩))
       (a, λx∈measure(int × int, %⟨a,b⟩. nat_of($- a $- b)) -`` {a}. negDivAlg(x))

lemmas negDivAlg_unfold:

      negDivAlg(a) =
      (%⟨a,b⟩ f.
          if #0 $≤ a $+ b ∨ b $≤ #0 then ⟨#-1, a $+ b⟩
          else adjust(b, f ` ⟨a, #2 $× b⟩))
       (a, λx∈measure(int × int, %⟨a,b⟩. nat_of($- a $- b)) -`` {a}. negDivAlg(x))

lemma negDivAlg_eqn:

      [| #0 $< b; a ∈ int; b ∈ int |]
      ==> negDivAlg(⟨a, b⟩) =
          (if #0 $≤ a $+ b then ⟨#-1, a $+ b⟩ else adjust(b, negDivAlg(⟨a, #2 $× b⟩)))

lemma negDivAlg_induct_lemma:

      (!!a b. [| a ∈ int; b ∈ int; ¬ (#0 $≤ a $+ b ∨ b $≤ #0) --> P(⟨a, #2 $× b⟩) |]
              ==> P(⟨a, b⟩))
      ==> ⟨u, v⟩ ∈ int × int --> P(⟨u, v⟩)

lemma negDivAlg_induct:

      [| u ∈ int; v ∈ int;
         !!a b. [| a ∈ int; b ∈ int; ¬ (#0 $≤ a $+ b ∨ b $≤ #0) --> P(a, #2 $× b) |]
                ==> P(a, b) |]
      ==> P(u, v)

lemma negDivAlg_type:

      [| a ∈ int; b ∈ int |] ==> negDivAlg(⟨a, b⟩) ∈ int × int

lemma negDivAlg_correct:

      [| a ∈ int; b ∈ int; a $< #0; #0 $< b |] ==> quorem(⟨a, b⟩, negDivAlg(⟨a, b⟩))

### Existence shown by proving the division algorithm to be correct

lemma quorem_0:

      [| b ≠ #0; b ∈ int |] ==> quorem(⟨#0, b⟩, ⟨#0, #0⟩)

lemma posDivAlg_zero_divisor:

      posDivAlg(⟨a, #0⟩) = ⟨#0, a⟩

lemma posDivAlg_0:

      posDivAlg(⟨#0, b⟩) = ⟨#0, #0⟩

lemma linear_arith_lemma:

      ¬ #0 $≤ #-1 $+ b ==> b $≤ #0

lemma negDivAlg_minus1:

      negDivAlg(⟨#-1, b⟩) = ⟨#-1, b $- #1⟩

lemma negateSnd_eq:

      negateSnd(⟨q, r⟩) = ⟨q, $- r⟩

lemma negateSnd_type:

      qr ∈ int × int ==> negateSnd(qr) ∈ int × int

lemma quorem_neg:

      [| quorem(⟨$- a, $- b⟩, qr); a ∈ int; b ∈ int; qr ∈ int × int |]
      ==> quorem(⟨a, b⟩, negateSnd(qr))

lemma divAlg_correct:

      [| b ≠ #0; a ∈ int; b ∈ int |] ==> quorem(⟨a, b⟩, divAlg(⟨a, b⟩))

lemma divAlg_type:

      [| a ∈ int; b ∈ int |] ==> divAlg(⟨a, b⟩) ∈ int × int

lemma zdiv_intify1:

      intify(x) zdiv y = x zdiv y

lemma zdiv_intify2:

      x zdiv intify(y) = x zdiv y

lemma zdiv_type:

      z zdiv w ∈ int

lemma zmod_intify1:

      intify(x) zmod y = x zmod y

lemma zmod_intify2:

      x zmod intify(y) = x zmod y

lemma zmod_type:

      z zmod w ∈ int

lemma DIVISION_BY_ZERO_ZDIV:

      a zdiv #0 = #0

lemma DIVISION_BY_ZERO_ZMOD:

      a zmod #0 = intify(a)

lemma raw_zmod_zdiv_equality:

      [| a ∈ int; b ∈ int |] ==> a = b $× (a zdiv b) $+ a zmod b

lemma zmod_zdiv_equality:

      intify(a) = b $× (a zdiv b) $+ a zmod b

lemma pos_mod:

      #0 $< b ==> #0 $≤ a zmod b ∧ a zmod b $< b

lemmas pos_mod_sign:

      #0 $< b ==> #0 $≤ a zmod b

and pos_mod_bound:

      #0 $< b ==> a zmod b $< b

lemmas pos_mod_sign:

      #0 $< b ==> #0 $≤ a zmod b

and pos_mod_bound:

      #0 $< b ==> a zmod b $< b

lemma neg_mod:

      b $< #0 ==> a zmod b $≤ #0 ∧ b $< a zmod b

lemmas neg_mod_sign:

      b $< #0 ==> a zmod b $≤ #0

and neg_mod_bound:

      b $< #0 ==> b $< a zmod b

lemmas neg_mod_sign:

      b $< #0 ==> a zmod b $≤ #0

and neg_mod_bound:

      b $< #0 ==> b $< a zmod b

lemma quorem_div_mod:

      [| b ≠ #0; a ∈ int; b ∈ int |] ==> quorem(⟨a, b⟩, ⟨a zdiv b, a zmod b⟩)

lemma quorem_div:

      [| quorem(⟨a, b⟩, ⟨q, r⟩); b ≠ #0; a ∈ int; b ∈ int; q ∈ int |] ==> a zdiv b = q

lemma quorem_mod:

      [| quorem(⟨a, b⟩, ⟨q, r⟩); b ≠ #0; a ∈ int; b ∈ int; q ∈ int; r ∈ int |]
      ==> a zmod b = r

lemma zdiv_pos_pos_trivial_raw:

      [| a ∈ int; b ∈ int; #0 $≤ a; a $< b |] ==> a zdiv b = #0

lemma zdiv_pos_pos_trivial:

      [| #0 $≤ a; a $< b |] ==> a zdiv b = #0

lemma zdiv_neg_neg_trivial_raw:

      [| a ∈ int; b ∈ int; a $≤ #0; b $< a |] ==> a zdiv b = #0

lemma zdiv_neg_neg_trivial:

      [| a $≤ #0; b $< a |] ==> a zdiv b = #0

lemma zadd_le_0_lemma:

      [| a $+ b $≤ #0; #0 $< a; #0 $< b |] ==> False

lemma zdiv_pos_neg_trivial_raw:

      [| a ∈ int; b ∈ int; #0 $< a; a $+ b $≤ #0 |] ==> a zdiv b = #-1

lemma zdiv_pos_neg_trivial:

      [| #0 $< a; a $+ b $≤ #0 |] ==> a zdiv b = #-1

lemma zmod_pos_pos_trivial_raw:

      [| a ∈ int; b ∈ int; #0 $≤ a; a $< b |] ==> a zmod b = a

lemma zmod_pos_pos_trivial:

      [| #0 $≤ a; a $< b |] ==> a zmod b = intify(a)

lemma zmod_neg_neg_trivial_raw:

      [| a ∈ int; b ∈ int; a $≤ #0; b $< a |] ==> a zmod b = a

lemma zmod_neg_neg_trivial:

      [| a $≤ #0; b $< a |] ==> a zmod b = intify(a)

lemma zmod_pos_neg_trivial_raw:

      [| a ∈ int; b ∈ int; #0 $< a; a $+ b $≤ #0 |] ==> a zmod b = a $+ b

lemma zmod_pos_neg_trivial:

      [| #0 $< a; a $+ b $≤ #0 |] ==> a zmod b = a $+ b

lemma zdiv_zminus_zminus_raw:

      [| a ∈ int; b ∈ int |] ==> $- a zdiv $- b = a zdiv b

lemma zdiv_zminus_zminus:

      $- a zdiv $- b = a zdiv b

lemma zmod_zminus_zminus_raw:

      [| a ∈ int; b ∈ int |] ==> $- a zmod $- b = $- (a zmod b)

lemma zmod_zminus_zminus:

      $- a zmod $- b = $- (a zmod b)

### division of a number by itself

lemma self_quotient_aux1:

      [| #0 $< a; a = r $+ a $× q; r $< a |] ==> #1 $≤ q

lemma self_quotient_aux2:

      [| #0 $< a; a = r $+ a $× q; #0 $≤ r |] ==> q $≤ #1

lemma self_quotient:

      [| quorem(⟨a, a⟩, ⟨q, r⟩); a ∈ int; q ∈ int; a ≠ #0 |] ==> q = #1

lemma self_remainder:

      [| quorem(⟨a, a⟩, ⟨q, r⟩); a ∈ int; q ∈ int; r ∈ int; a ≠ #0 |] ==> r = #0

lemma zdiv_self_raw:

      [| a ≠ #0; a ∈ int |] ==> a zdiv a = #1

lemma zdiv_self:

      intify(a) ≠ #0 ==> a zdiv a = #1

lemma zmod_self_raw:

      a ∈ int ==> a zmod a = #0

lemma zmod_self:

      a zmod a = #0

### Computation of division and remainder

lemma zdiv_zero:

      #0 zdiv b = #0

lemma zdiv_eq_minus1:

      #0 $< b ==> #-1 zdiv b = #-1

lemma zmod_zero:

      #0 zmod b = #0

lemma zdiv_minus1:

      #0 $< b ==> #-1 zdiv b = #-1

lemma zmod_minus1:

      #0 $< b ==> #-1 zmod b = b $- #1

lemma zdiv_pos_pos:

      [| #0 $< a; #0 $≤ b |] ==> a zdiv b = fst(posDivAlg(⟨intify(a), intify(b)⟩))

lemma zmod_pos_pos:

      [| #0 $< a; #0 $≤ b |] ==> a zmod b = snd(posDivAlg(⟨intify(a), intify(b)⟩))

lemma zdiv_neg_pos:

      [| a $< #0; #0 $< b |] ==> a zdiv b = fst(negDivAlg(⟨intify(a), intify(b)⟩))

lemma zmod_neg_pos:

      [| a $< #0; #0 $< b |] ==> a zmod b = snd(negDivAlg(⟨intify(a), intify(b)⟩))

lemma zdiv_pos_neg:

      [| #0 $< a; b $< #0 |] ==> a zdiv b = fst(negateSnd(negDivAlg(⟨$- a, $- b⟩)))

lemma zmod_pos_neg:

      [| #0 $< a; b $< #0 |] ==> a zmod b = snd(negateSnd(negDivAlg(⟨$- a, $- b⟩)))

lemma zdiv_neg_neg:

      [| a $< #0; b $≤ #0 |] ==> a zdiv b = fst(negateSnd(posDivAlg(⟨$- a, $- b⟩)))

lemma zmod_neg_neg:

      [| a $< #0; b $≤ #0 |] ==> a zmod b = snd(negateSnd(posDivAlg(⟨$- a, $- b⟩)))

lemma zmod_1:

      a zmod #1 = #0

lemma zdiv_1:

      a zdiv #1 = intify(a)

lemma zmod_minus1_right:

      a zmod #-1 = #0

lemma zdiv_minus1_right_raw:

      a ∈ int ==> a zdiv #-1 = $- a

lemma zdiv_minus1_right:

      a zdiv #-1 = $- a

### Monotonicity in the first argument (divisor)

lemma zdiv_mono1:

      [| a $≤ a'; #0 $< b |] ==> a zdiv b $≤ a' zdiv b

lemma zdiv_mono1_neg:

      [| a $≤ a'; b $< #0 |] ==> a' zdiv b $≤ a zdiv b

### Monotonicity in the second argument (dividend)

lemma q_pos_lemma:

      [| #0 $≤ b' $× q' $+ r'; r' $< b'; #0 $< b' |] ==> #0 $≤ q'

lemma zdiv_mono2_lemma:

      [| b $× q $+ r = b' $× q' $+ r'; #0 $≤ b' $× q' $+ r'; r' $< b'; #0 $≤ r;
         #0 $< b'; b' $≤ b |]
      ==> q $≤ q'

lemma zdiv_mono2_raw:

      [| #0 $≤ a; #0 $< b'; b' $≤ b; a ∈ int |] ==> a zdiv b $≤ a zdiv b'

lemma zdiv_mono2:

      [| #0 $≤ a; #0 $< b'; b' $≤ b |] ==> a zdiv b $≤ a zdiv b'

lemma q_neg_lemma:

      [| b' $× q' $+ r' $< #0; #0 $≤ r'; #0 $< b' |] ==> q' $< #0

lemma zdiv_mono2_neg_lemma:

      [| b $× q $+ r = b' $× q' $+ r'; b' $× q' $+ r' $< #0; r $< b; #0 $≤ r';
         #0 $< b'; b' $≤ b |]
      ==> q' $≤ q

lemma zdiv_mono2_neg_raw:

      [| a $< #0; #0 $< b'; b' $≤ b; a ∈ int |] ==> a zdiv b' $≤ a zdiv b

lemma zdiv_mono2_neg:

      [| a $< #0; #0 $< b'; b' $≤ b |] ==> a zdiv b' $≤ a zdiv b

### More algebraic laws for zdiv and zmod

lemma zmult1_lemma:

      [| quorem(⟨b, c⟩, ⟨q, r⟩); c ∈ int; c ≠ #0 |]
      ==> quorem(⟨a $× b, c⟩, ⟨a $× q $+ a $× r zdiv c, a $× r zmod c⟩)

lemma zdiv_zmult1_eq_raw:

      [| b ∈ int; c ∈ int |]
      ==> a $× b zdiv c = a $× (b zdiv c) $+ a $× (b zmod c) zdiv c

lemma zdiv_zmult1_eq:

      a $× b zdiv c = a $× (b zdiv c) $+ a $× (b zmod c) zdiv c

lemma zmod_zmult1_eq_raw:

      [| b ∈ int; c ∈ int |] ==> a $× b zmod c = a $× (b zmod c) zmod c

lemma zmod_zmult1_eq:

      a $× b zmod c = a $× (b zmod c) zmod c

lemma zmod_zmult1_eq':

      a $× b zmod c = a zmod c $× b zmod c

lemma zmod_zmult_distrib:

      a $× b zmod c = a zmod c $× (b zmod c) zmod c

lemma zdiv_zmult_self1:

      intify(b) ≠ #0 ==> a $× b zdiv b = intify(a)

lemma zdiv_zmult_self2:

      intify(b) ≠ #0 ==> b $× a zdiv b = intify(a)

lemma zmod_zmult_self1:

      a $× b zmod b = #0

lemma zmod_zmult_self2:

      b $× a zmod b = #0

lemma zadd1_lemma:

      [| quorem(⟨a, c⟩, ⟨aq, ar⟩); quorem(⟨b, c⟩, ⟨bq, br⟩); c ∈ int; c ≠ #0 |]
      ==> quorem(⟨a $+ b, c⟩, ⟨aq $+ bq $+ (ar $+ br) zdiv c, (ar $+ br) zmod c⟩)

lemma zdiv_zadd1_eq_raw:

      [| a ∈ int; b ∈ int; c ∈ int |]
      ==> (a $+ b) zdiv c = a zdiv c $+ b zdiv c $+ (a zmod c $+ b zmod c) zdiv c

lemma zdiv_zadd1_eq:

      (a $+ b) zdiv c = a zdiv c $+ b zdiv c $+ (a zmod c $+ b zmod c) zdiv c

lemma zmod_zadd1_eq_raw:

      [| a ∈ int; b ∈ int; c ∈ int |]
      ==> (a $+ b) zmod c = (a zmod c $+ b zmod c) zmod c

lemma zmod_zadd1_eq:

      (a $+ b) zmod c = (a zmod c $+ b zmod c) zmod c

lemma zmod_div_trivial_raw:

      [| a ∈ int; b ∈ int |] ==> a zmod b zdiv b = #0

lemma zmod_div_trivial:

      a zmod b zdiv b = #0

lemma zmod_mod_trivial_raw:

      [| a ∈ int; b ∈ int |] ==> a zmod b zmod b = a zmod b

lemma zmod_mod_trivial:

      a zmod b zmod b = a zmod b

lemma zmod_zadd_left_eq:

      (a $+ b) zmod c = (a zmod c $+ b) zmod c

lemma zmod_zadd_right_eq:

      (a $+ b) zmod c = (a $+ b zmod c) zmod c

lemma zdiv_zadd_self1:

      intify(a) ≠ #0 ==> (a $+ b) zdiv a = b zdiv a $+ #1

lemma zdiv_zadd_self2:

      intify(a) ≠ #0 ==> (b $+ a) zdiv a = b zdiv a $+ #1

lemma zmod_zadd_self1:

      (a $+ b) zmod a = b zmod a

lemma zmod_zadd_self2:

      (b $+ a) zmod a = b zmod a

### proving a zdiv (b*c) = (a zdiv b) zdiv c

lemma zdiv_zmult2_aux1:

      [| #0 $< c; b $< r; r $≤ #0 |] ==> b $× c $< b $× (q zmod c) $+ r

lemma zdiv_zmult2_aux2:

      [| #0 $< c; b $< r; r $≤ #0 |] ==> b $× (q zmod c) $+ r $≤ #0

lemma zdiv_zmult2_aux3:

      [| #0 $< c; #0 $≤ r; r $< b |] ==> #0 $≤ b $× (q zmod c) $+ r

lemma zdiv_zmult2_aux4:

      [| #0 $< c; #0 $≤ r; r $< b |] ==> b $× (q zmod c) $+ r $< b $× c

lemma zdiv_zmult2_lemma:

      [| quorem(⟨a, b⟩, ⟨q, r⟩); a ∈ int; b ∈ int; b ≠ #0; #0 $< c |]
      ==> quorem(⟨a, b $× c⟩, ⟨q zdiv c, b $× (q zmod c) $+ r⟩)

lemma zdiv_zmult2_eq_raw:

      [| #0 $< c; a ∈ int; b ∈ int |] ==> a zdiv (b $× c) = a zdiv b zdiv c

lemma zdiv_zmult2_eq:

      #0 $< c ==> a zdiv (b $× c) = a zdiv b zdiv c

lemma zmod_zmult2_eq_raw:

      [| #0 $< c; a ∈ int; b ∈ int |]
      ==> a zmod (b $× c) = b $× (a zdiv b zmod c) $+ a zmod b

lemma zmod_zmult2_eq:

      #0 $< c ==> a zmod (b $× c) = b $× (a zdiv b zmod c) $+ a zmod b

### Cancellation of common factors in "zdiv"

lemma zdiv_zmult_zmult1_aux1:

      [| #0 $< b; intify(c) ≠ #0 |] ==> c $× a zdiv (c $× b) = a zdiv b

lemma zdiv_zmult_zmult1_aux2:

      [| b $< #0; intify(c) ≠ #0 |] ==> c $× a zdiv (c $× b) = a zdiv b

lemma zdiv_zmult_zmult1_raw:

      [| intify(c) ≠ #0; b ∈ int |] ==> c $× a zdiv (c $× b) = a zdiv b

lemma zdiv_zmult_zmult1:

      intify(c) ≠ #0 ==> c $× a zdiv (c $× b) = a zdiv b

lemma zdiv_zmult_zmult2:

      intify(c) ≠ #0 ==> a $× c zdiv (b $× c) = a zdiv b

### Distribution of factors over "zmod"

lemma zmod_zmult_zmult1_aux1:

      [| #0 $< b; intify(c) ≠ #0 |] ==> c $× a zmod (c $× b) = c $× (a zmod b)

lemma zmod_zmult_zmult1_aux2:

      [| b $< #0; intify(c) ≠ #0 |] ==> c $× a zmod (c $× b) = c $× (a zmod b)

lemma zmod_zmult_zmult1_raw:

      [| b ∈ int; c ∈ int |] ==> c $× a zmod (c $× b) = c $× (a zmod b)

lemma zmod_zmult_zmult1:

      c $× a zmod (c $× b) = c $× (a zmod b)

lemma zmod_zmult_zmult2:

      a $× c zmod (b $× c) = a zmod b $× c

lemma zdiv_neg_pos_less0:

      [| a $< #0; #0 $< b |] ==> a zdiv b $< #0

lemma zdiv_nonneg_neg_le0:

      [| #0 $≤ a; b $< #0 |] ==> a zdiv b $≤ #0

lemma pos_imp_zdiv_nonneg_iff:

      #0 $< b ==> #0 $≤ a zdiv b <-> #0 $≤ a

lemma neg_imp_zdiv_nonneg_iff:

      b $< #0 ==> #0 $≤ a zdiv b <-> a $≤ #0

lemma pos_imp_zdiv_neg_iff:

      #0 $< b ==> a zdiv b $< #0 <-> a $< #0

lemma neg_imp_zdiv_neg_iff:

      b $< #0 ==> a zdiv b $< #0 <-> #0 $< a