# Theory IntArith

Up to index of Isabelle/ZF

theory IntArith
imports Bin
uses int_arith.ML
begin

    theory IntArith imports Bin
    uses "int_arith.ML" begin

    end

theorem zless_iff_zdiff_zless_0:

      x $< y <-> x $- y $< #0

theorem eq_iff_zdiff_eq_0:

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

theorem zle_iff_zdiff_zle_0:

      x $≤ y <-> x $- y $≤ #0

theorem left_zadd_zmult_distrib:

      i $× u $+ (j $× u $+ k) = (i $+ j) $× u $+ k

theorem eq_add_iff1:

      i $× u $+ m = j $× u $+ n <-> (i $- j) $× u $+ m = intify(n)

theorem eq_add_iff2:

      i $× u $+ m = j $× u $+ n <-> intify(m) = (j $- i) $× u $+ n

theorem less_add_iff1:

      i $× u $+ m $< j $× u $+ n <-> (i $- j) $× u $+ m $< n

theorem less_add_iff2:

      i $× u $+ m $< j $× u $+ n <-> m $< (j $- i) $× u $+ n

theorem le_add_iff1:

      i $× u $+ m $≤ j $× u $+ n <-> (i $- j) $× u $+ m $≤ n

theorem le_add_iff2:

      i $× u $+ m $≤ j $× u $+ n <-> m $≤ (j $- i) $× u $+ n