Documentation

Init.Data.Int.DivMod.Lemmas

Further lemmas about integer division, now that omega is available. #

@[simp]
theorem Int.natCast_eq_zero {n : Nat} :
n = 0 n = 0
theorem Int.exists_add_of_le {a b : Int} (h : a b) :
(c : Nat), b = a + c
theorem Int.toNat_emod {x y : Int} (hx : 0 x) (hy : 0 y) :
(x % y).toNat = x.toNat % y.toNat

dvd #

theorem Int.dvd_antisymm {a b : Int} (H1 : 0 a) (H2 : 0 b) :
a bb aa = b
theorem Int.dvd_add {a b c : Int} :
a ba ca b + c
theorem Int.dvd_sub {a b c : Int} :
a ba ca b - c
theorem Int.dvd_add_left {a b c : Int} (H : a c) :
a b + c a b
theorem Int.dvd_add_right {a b c : Int} (H : a b) :
a b + c a c
@[simp]
theorem Int.dvd_add_mul_self {a b c : Int} :
a b + c * a a b
@[simp]
theorem Int.dvd_add_self_mul {a b c : Int} :
a b + a * c a b
@[simp]
theorem Int.dvd_mul_self_add {a b c : Int} :
a b * a + c a c
@[simp]
theorem Int.dvd_self_mul_add {a b c : Int} :
a a * b + c a c
theorem Int.dvd_iff_dvd_of_dvd_sub {a b c : Int} (H : a b - c) :
a b a c
theorem Int.dvd_iff_dvd_of_dvd_add {a b c : Int} (H : a b + c) :
a b a c
theorem Int.le_of_dvd {a b : Int} (bpos : 0 < b) (H : a b) :
a b
theorem Int.natAbs_dvd {a b : Int} :
a.natAbs b a b
theorem Int.dvd_natAbs {a b : Int} :
a b.natAbs a b
theorem Int.natAbs_dvd_self {a : Int} :
a.natAbs a
theorem Int.dvd_natAbs_self {a : Int} :
a a.natAbs
theorem Int.natAbs_eq_of_dvd_dvd {m n : Int} (hmn : m n) (hnm : n m) :
theorem Int.ofNat_dvd_right {n : Nat} {z : Int} :
z n z.natAbs n
@[simp]
theorem Int.negSucc_dvd {a : Nat} {b : Int} :
negSucc a b ↑(a + 1) b
@[simp]
theorem Int.dvd_negSucc {a : Int} {b : Nat} :
a negSucc b a ↑(b + 1)
theorem Int.eq_one_of_dvd_one {a : Int} (H : 0 a) (H' : a 1) :
a = 1
theorem Int.eq_one_of_mul_eq_one_right {a b : Int} (H : 0 a) (H' : a * b = 1) :
a = 1
theorem Int.eq_one_of_mul_eq_one_left {a b : Int} (H : 0 b) (H' : a * b = 1) :
b = 1
instance Int.decidableDvd :
DecidableRel fun (x1 x2 : Int) => x1 x2
Equations
    theorem Int.mul_dvd_mul_iff_left {a b c : Int} (h : a 0) :
    a * b a * c b c
    theorem Int.mul_dvd_mul_iff_right {a b c : Int} (h : a 0) :
    b * a c * a b c
    theorem Int.mul_dvd_mul {a b c d : Int} :
    a bc da * c b * d
    theorem Int.mul_dvd_mul_left {b c : Int} (a : Int) (h : b c) :
    a * b a * c
    theorem Int.mul_dvd_mul_right {b c : Int} (a : Int) (h : b c) :
    b * a c * a
    theorem Int.dvd_of_mul_dvd_mul_left {a m n : Int} (ha : a 0) (h : a * m a * n) :
    m n
    theorem Int.dvd_of_mul_dvd_mul_right {a m n : Int} (ha : a 0) (h : m * a n * a) :
    m n
    theorem Int.natCast_dvd_natCast {m n : Nat} :
    m n m n

    *div zero #

    @[simp]
    theorem Int.zero_tdiv (b : Int) :
    tdiv 0 b = 0
    @[simp]
    theorem Int.tdiv_zero (a : Int) :
    a.tdiv 0 = 0
    @[simp]
    theorem Int.zero_fdiv (b : Int) :
    fdiv 0 b = 0
    @[simp]
    theorem Int.fdiv_zero (a : Int) :
    a.fdiv 0 = 0

    preliminaries for div equivalences #

    theorem Int.negSucc_emod_ofNat_succ_eq_zero_iff {a b : Nat} :
    negSucc a % (b + 1) = 0 (a + 1) % (b + 1) = 0
    theorem Int.negSucc_emod_negSucc_eq_zero_iff {a b : Nat} :
    negSucc a % negSucc b = 0 (a + 1) % (b + 1) = 0

    div equivalences #

    theorem Int.tdiv_eq_ediv_of_nonneg {a b : Int} :
    0 aa.tdiv b = a / b
    theorem Int.tdiv_eq_ediv {a b : Int} :
    a.tdiv b = a / b + if 0 a b a then 0 else b.sign
    theorem Int.ediv_eq_tdiv {a b : Int} :
    a / b = a.tdiv b - if 0 a b a then 0 else b.sign
    theorem Int.divExact_eq_tdiv {a b : Int} (h : b a) :
    a.divExact b h = a.tdiv b
    theorem Int.fdiv_eq_ediv_of_nonneg (a : Int) {b : Int} :
    0 ba.fdiv b = a / b
    theorem Int.fdiv_eq_ediv {a b : Int} :
    a.fdiv b = a / b - if 0 b b a then 0 else 1
    theorem Int.ediv_eq_fdiv {a b : Int} :
    a / b = a.fdiv b + if 0 b b a then 0 else 1
    theorem Int.divExact_eq_fdiv {a b : Int} (h : b a) :
    a.divExact b h = a.fdiv b
    theorem Int.fdiv_eq_tdiv_of_nonneg {a b : Int} (Ha : 0 a) (Hb : 0 b) :
    a.fdiv b = a.tdiv b
    theorem Int.fdiv_eq_tdiv {a b : Int} :
    a.fdiv b = a.tdiv b - if b a then 0 else if 0 a then if 0 b then 0 else 1 else if 0 b then b.sign else 1 + b.sign
    theorem Int.tdiv_eq_fdiv {a b : Int} :
    a.tdiv b = a.fdiv b + if b a then 0 else if 0 a then if 0 b then 0 else 1 else if 0 b then b.sign else 1 + b.sign
    theorem Int.tdiv_eq_ediv_of_dvd {a b : Int} (h : b a) :
    a.tdiv b = a / b
    theorem Int.fdiv_eq_ediv_of_dvd {a b : Int} (h : b a) :
    a.fdiv b = a / b

    mod zero #

    @[simp]
    theorem Int.zero_tmod (b : Int) :
    tmod 0 b = 0
    @[simp]
    theorem Int.tmod_zero (a : Int) :
    a.tmod 0 = a
    @[simp]
    theorem Int.zero_fmod (b : Int) :
    fmod 0 b = 0
    @[simp]
    theorem Int.fmod_zero (a : Int) :
    a.fmod 0 = a

    mod definitions #

    theorem Int.tmod_add_tdiv (a b : Int) :
    a.tmod b + b * a.tdiv b = a
    theorem Int.tdiv_add_tmod (a b : Int) :
    b * a.tdiv b + a.tmod b = a
    theorem Int.tmod_add_tdiv' (m k : Int) :
    m.tmod k + m.tdiv k * k = m

    Variant of tmod_add_tdiv with the multiplication written the other way around.

    theorem Int.tdiv_add_tmod' (m k : Int) :
    m.tdiv k * k + m.tmod k = m

    Variant of tdiv_add_tmod with the multiplication written the other way around.

    theorem Int.tmod_def (a b : Int) :
    a.tmod b = a - b * a.tdiv b
    theorem Int.fmod_add_fdiv (a b : Int) :
    a.fmod b + b * a.fdiv b = a
    theorem Int.fmod_add_fdiv' (a b : Int) :
    a.fmod b + a.fdiv b * b = a

    Variant of fmod_add_fdiv with the multiplication written the other way around.

    theorem Int.fdiv_add_fmod (a b : Int) :
    b * a.fdiv b + a.fmod b = a
    theorem Int.fdiv_add_fmod' (a b : Int) :
    a.fdiv b * b + a.fmod b = a

    Variant of fdiv_add_fmod with the multiplication written the other way around.

    theorem Int.fmod_def (a b : Int) :
    a.fmod b = a - b * a.fdiv b

    mod equivalences #

    theorem Int.fmod_eq_emod_of_nonneg (a : Int) {b : Int} (hb : 0 b) :
    a.fmod b = a % b
    theorem Int.fmod_eq_emod {a b : Int} :
    a.fmod b = a % b + if 0 b b a then 0 else b
    theorem Int.emod_eq_fmod {a b : Int} :
    a % b = a.fmod b - if 0 b b a then 0 else b
    theorem Int.tmod_eq_emod_of_nonneg {a b : Int} (ha : 0 a) :
    a.tmod b = a % b
    theorem Int.tmod_eq_emod {a b : Int} :
    a.tmod b = a % b - ↑(if 0 a b a then 0 else b.natAbs)
    theorem Int.emod_eq_tmod {a b : Int} :
    a % b = a.tmod b + ↑(if 0 a b a then 0 else b.natAbs)
    theorem Int.fmod_eq_tmod_of_nonneg {a b : Int} (ha : 0 a) (hb : 0 b) :
    a.fmod b = a.tmod b
    theorem Int.fmod_eq_tmod {a b : Int} :
    a.fmod b = a.tmod b + if b a then 0 else if 0 a then if 0 b then 0 else b else if 0 b then b.natAbs else 2 * b.toNat
    theorem Int.tmod_eq_fmod {a b : Int} :
    a.tmod b = a.fmod b - if b a then 0 else if 0 a then if 0 b then 0 else b else if 0 b then b.natAbs else 2 * b.toNat

    / ediv #

    theorem Int.mul_add_ediv_right (a c : Int) {b : Int} (H : b 0) :
    (a * b + c) / b = a + c / b
    theorem Int.mul_add_ediv_left (b : Int) {a : Int} (c : Int) (H : a 0) :
    (a * b + c) / a = b + c / a
    theorem Int.sub_mul_ediv_right (a b : Int) {c : Int} (H : c 0) :
    (a - b * c) / c = a / c - b
    theorem Int.sub_mul_ediv_left (a : Int) {b : Int} (c : Int) (H : b 0) :
    (a - b * c) / b = a / b - c
    theorem Int.mul_sub_ediv_right (a c : Int) {b : Int} (H : b 0) :
    (a * b - c) / b = a + -c / b
    theorem Int.mul_sub_ediv_left (b : Int) {a : Int} (c : Int) (H : a 0) :
    (a * b - c) / a = b + -c / a
    theorem Int.ediv_neg_of_neg_of_pos {a b : Int} (Ha : a < 0) (Hb : 0 < b) :
    a / b < 0
    @[reducible, inline, deprecated Int.ediv_neg_of_neg_of_pos (since := "2025-03-04")]
    abbrev Int.ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) :
    a / b < 0
    Equations
      Instances For
        theorem Int.negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) :
        negSucc m / b = -((↑m).ediv b + 1)
        theorem Int.ediv_nonneg {a b : Int} (Ha : 0 a) (Hb : 0 b) :
        0 a / b
        theorem Int.ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a 0) (Hb : b 0) :
        0 a / b
        theorem Int.ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) :
        0 < a / b
        theorem Int.ediv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) :
        a / b 0
        @[reducible, inline, deprecated Int.ediv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
        abbrev Int.ediv_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) :
        a / b 0
        Equations
          Instances For
            theorem Int.ediv_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) :
            a / b = 0
            theorem Int.ediv_eq_neg_one_of_neg_of_le {a b : Int} (H1 : a < 0) (H2 : -a b) :
            a / b = -1
            theorem Int.ediv_eq_one_of_neg_of_le {a b : Int} (H1 : a < 0) (H2 : b a) :
            a / b = 1
            theorem Int.one_ediv (b : Int) :
            1 / b = if b.natAbs = 1 then b else 0
            theorem Int.neg_one_ediv (b : Int) :
            -1 / b = -b.sign
            @[simp]
            theorem Int.mul_ediv_mul_of_pos {a : Int} (b c : Int) (H : 0 < a) :
            a * b / (a * c) = b / c
            @[simp]
            theorem Int.mul_ediv_mul_of_pos_left (a : Int) {b : Int} (c : Int) (H : 0 < b) :
            a * b / (c * b) = a / c
            theorem Int.ediv_eq_of_eq_mul_right {a b c : Int} (H1 : b 0) (H2 : a = b * c) :
            a / b = c
            theorem Int.eq_ediv_of_mul_eq_right {a b c : Int} (H1 : a 0) (H2 : a * b = c) :
            b = c / a
            theorem Int.ediv_eq_of_eq_mul_left {a b c : Int} (H1 : b 0) (H2 : a = c * b) :
            a / b = c
            theorem Int.eq_ediv_of_mul_eq_left {a b c : Int} (H1 : b 0) (H2 : a * b = c) :
            a = c / b
            @[simp]
            theorem Int.ediv_self {a : Int} (H : a 0) :
            a / a = 1
            @[simp]
            theorem Int.neg_ediv_self (a : Int) (h : a 0) :
            -a / a = -1
            theorem Int.sign_ediv (a b : Int) :
            (a / b).sign = if 0 a a < b.natAbs then 0 else a.sign * b.sign

            emod #

            theorem Int.mod_def' (m n : Int) :
            m % n = m.emod n
            theorem Int.negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) :
            negSucc m % b = b - 1 - m % b
            theorem Int.emod_negSucc (m : Nat) (n : Int) :
            theorem Int.ofNat_mod_ofNat (m n : Nat) :
            m % n = ↑(m % n)
            @[simp]
            theorem Int.add_neg_mul_emod_self_right (a b c : Int) :
            (a + -(b * c)) % c = a % c
            @[deprecated Int.add_neg_mul_emod_self_right (since := "2025-04-11")]
            theorem Int.add_neg_mul_emod_self {a b c : Int} :
            (a + -(b * c)) % c = a % c
            @[simp]
            theorem Int.add_neg_mul_emod_self_left (a b c : Int) :
            (a + -(b * c)) % b = a % b
            @[simp]
            theorem Int.add_emod_right (a b : Int) :
            (a + b) % b = a % b
            @[deprecated Int.add_emod_right (since := "2025-04-11")]
            theorem Int.add_emod_self {a b : Int} :
            (a + b) % b = a % b
            @[simp]
            theorem Int.add_emod_left (a b : Int) :
            (a + b) % a = b % a
            @[deprecated Int.add_emod_left (since := "2025-04-11")]
            theorem Int.add_emod_self_left {a b : Int} :
            (a + b) % a = b % a
            @[simp]
            theorem Int.sub_mul_emod_self_right (a b c : Int) :
            (a - b * c) % c = a % c
            @[simp]
            theorem Int.sub_mul_emod_self_left (a b c : Int) :
            (a - b * c) % b = a % b
            @[simp]
            theorem Int.mul_sub_emod_self_right (a b c : Int) :
            (a * b - c) % b = -c % b
            @[simp]
            theorem Int.mul_sub_emod_self_left (a b c : Int) :
            (a * b - c) % a = -c % a
            @[simp]
            theorem Int.sub_emod_right (a b : Int) :
            (a - b) % b = a % b
            @[simp]
            theorem Int.sub_emod_left (a b : Int) :
            (a - b) % a = -b % a
            theorem Int.neg_emod_eq_sub_emod {a b : Int} :
            -a % b = (b - a) % b
            theorem Int.emod_eq_add_self_emod {a b : Int} :
            a % b = (a + b) % b
            @[simp]
            theorem Int.emod_neg (a b : Int) :
            a % -b = a % b
            @[simp]
            theorem Int.neg_emod_self (a : Int) :
            -a % a = 0
            @[simp]
            theorem Int.emod_sub_emod (m n k : Int) :
            (m % n - k) % n = (m - k) % n
            @[simp]
            theorem Int.sub_emod_emod (m n k : Int) :
            (m - n % k) % k = (m - n) % k
            theorem Int.emod_eq_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) :
            a % b = a
            theorem Int.emod_lt_of_neg (a : Int) {b : Int} (h : b < 0) :
            a % b < -b
            theorem Int.emod_lt (a : Int) {b : Int} (h : b 0) :
            a % b < b.natAbs
            @[simp]
            theorem Int.emod_self_add_one {x : Int} (h : 0 x) :
            x % (x + 1) = x
            theorem Int.sign_emod (a : Int) {b : Int} (h : b 0) :
            (a % b).sign = if b a then 0 else 1
            theorem Int.one_emod {b : Int} :
            1 % b = if b.natAbs = 1 then 0 else 1
            @[simp]
            theorem Int.neg_emod_two (i : Int) :
            -i % 2 = i % 2

            properties of / and % #

            theorem Int.mul_ediv_cancel_of_dvd {a b : Int} (H : b a) :
            b * (a / b) = a
            theorem Int.ediv_mul_cancel_of_dvd {a b : Int} (H : b a) :
            a / b * b = a
            theorem Int.emod_two_eq (x : Int) :
            x % 2 = 0 x % 2 = 1
            theorem Int.add_emod_eq_add_emod_left {m n k : Int} (i : Int) (H : m % n = k % n) :
            (i + m) % n = (i + k) % n
            theorem Int.emod_add_cancel_left {m n k i : Int} :
            (i + m) % n = (i + k) % n m % n = k % n
            theorem Int.emod_sub_cancel_right {m n k : Int} (i : Int) :
            (m - i) % n = (k - i) % n m % n = k % n
            theorem Int.emod_eq_emod_iff_emod_sub_eq_zero {m n k : Int} :
            m % n = k % n (m - k) % n = 0
            theorem Int.emod_sub_cancel_left {m n k : Int} (i : Int) :
            (i - m) % n = (i - k) % n m % n = k % n
            theorem Int.ediv_emod_unique {a b r q : Int} (h : 0 < b) :
            a / b = q a % b = r r + b * q = a 0 r r < b
            theorem Int.ediv_emod_unique' {a b r q : Int} (h : b < 0) :
            a / b = q a % b = r r + b * q = a 0 r r < -b
            @[simp]
            theorem Int.mul_emod_mul_of_pos {a : Int} (b c : Int) (H : 0 < a) :
            a * b % (a * c) = a * (b % c)
            theorem Int.lt_ediv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) :
            a < (a / b + 1) * b
            theorem Int.neg_ediv {a b : Int} :
            -a / b = -(a / b) - if b a then 0 else b.sign
            theorem Int.tdiv_cases (n m : Int) :
            n.tdiv m = if 0 n then if 0 m then n / m else -(n / -m) else if 0 m then -(-n / m) else -n / -m
            theorem Int.neg_emod {a b : Int} :
            -a % b = if b a then 0 else b.natAbs - a % b
            theorem Int.natAbs_ediv (a b : Int) :
            (a / b).natAbs = a.natAbs / b.natAbs + if 0 a b = 0 b a then 0 else 1
            theorem Int.natAbs_ediv_of_nonneg {a b : Int} (ha : 0 a) :
            (a / b).natAbs = a.natAbs / b.natAbs
            theorem Int.natAbs_ediv_of_dvd {a b : Int} (hab : b a) :
            (a / b).natAbs = a.natAbs / b.natAbs
            theorem Int.natAbs_emod_of_nonneg {a : Int} (h : 0 a) (b : Int) :
            (a % b).natAbs = a.natAbs % b.natAbs
            theorem Int.natAbs_emod (a : Int) {b : Int} (hb : b 0) :
            (a % b).natAbs = if 0 a b a then a.natAbs % b.natAbs else b.natAbs - a.natAbs % b.natAbs
            theorem Int.natAbs_ediv_le_natAbs.aux (a : Int) (n : Nat) :
            (a / n).natAbs a.natAbs
            @[reducible, inline, deprecated Int.natAbs_ediv_le_natAbs (since := "2025-03-05")]
            abbrev Int.natAbs_div_le_natAbs (a b : Int) :
            (a / b).natAbs a.natAbs
            Equations
              Instances For
                theorem Int.ediv_le_self {a : Int} (b : Int) (Ha : 0 a) :
                a / b a
                theorem Int.dvd_emod_sub_self {x m : Int} :
                m x % m - x
                theorem Int.dvd_self_sub_emod {x m : Int} :
                m x - x % m
                theorem Int.emod_eq_iff {a b c : Int} (hb : b 0) :
                a % b = c 0 c c < b.natAbs b c - a
                @[simp]
                theorem Int.neg_mul_emod_left (a b : Int) :
                -(a * b) % b = 0
                @[simp]
                theorem Int.neg_mul_emod_right (a b : Int) :
                -(a * b) % a = 0
                @[deprecated Int.mul_ediv_cancel (since := "2025-03-05")]
                theorem Int.neg_mul_ediv_cancel (a b : Int) (h : b 0) :
                -(a * b) / b = -a
                @[deprecated Int.mul_ediv_cancel (since := "2025-03-05")]
                theorem Int.neg_mul_ediv_cancel_left (a b : Int) (h : a 0) :
                -(a * b) / a = -b
                @[simp]
                theorem Int.ediv_one (a : Int) :
                a / 1 = a
                @[simp]
                theorem Int.emod_one (a : Int) :
                a % 1 = 0
                @[deprecated Int.sub_emod_right (since := "2025-04-11")]
                theorem Int.emod_sub_cancel (x y : Int) :
                (x - y) % y = x % y
                @[simp]
                theorem Int.add_neg_emod_self (a b : Int) :
                (a + -b) % b = a % b
                @[simp]
                theorem Int.neg_add_emod_self (a b : Int) :
                (-a + b) % a = b % a
                theorem Int.dvd_self_sub_of_emod_eq {a b c : Int} :
                a % b = cb a - c

                If a % b = c then b divides a - c.

                @[deprecated Int.dvd_self_sub_of_emod_eq (since := "2025-04-12")]
                theorem Int.dvd_sub_of_emod_eq {a b c : Int} :
                a % b = cb a - c
                theorem Int.dvd_sub_self_of_emod_eq {a b c : Int} :
                a % b = cb c - a
                theorem Int.eq_mul_of_ediv_eq_right {a b c : Int} (H1 : b a) (H2 : a / b = c) :
                a = b * c
                theorem Int.ediv_eq_iff_eq_mul_right {a b c : Int} (H : b 0) (H' : b a) :
                a / b = c a = b * c
                theorem Int.ediv_eq_iff_eq_mul_left {a b c : Int} (H : b 0) (H' : b a) :
                a / b = c a = c * b
                theorem Int.eq_mul_of_ediv_eq_left {a b c : Int} (H1 : b a) (H2 : a / b = c) :
                a = c * b
                theorem Int.eq_zero_of_ediv_eq_zero {d n : Int} (h : d n) (H : n / d = 0) :
                n = 0
                theorem Int.sub_ediv_of_dvd_sub {a b c : Int} (hcab : c a - b) :
                (a - b) / c = a / c - b / c
                @[simp]
                theorem Int.ediv_left_inj {a b d : Int} (hda : d a) (hdb : d b) :
                a / d = b / d a = b
                theorem Int.ediv_sign (a b : Int) :
                a / b.sign = a * b.sign
                theorem Int.dvd_mul_of_ediv_dvd {a b c : Int} (h : b a) (hdiv : a / b c) :
                a b * c
                @[simp]
                theorem Int.ediv_dvd_iff_dvd_mul {a b c : Int} (h : b a) (hb : b 0) :
                a / b c a b * c
                theorem Int.mul_dvd_of_dvd_ediv {a b c : Int} (hcb : c b) (h : a b / c) :
                c * a b
                theorem Int.dvd_ediv_of_mul_dvd {a b c : Int} (h : a * b c) :
                b c / a
                @[simp]
                theorem Int.dvd_ediv_iff_mul_dvd {a b c : Int} (hbc : c b) :
                a b / c c * a b
                theorem Int.ediv_dvd_ediv {a b c : Int} :
                a bb cb / a c / a
                theorem Int.ediv_dvd_of_dvd {m n : Int} (hmn : m n) :
                n / m n
                theorem Int.emod_natAbs_of_nonneg {x : Int} (h : 0 x) {n : Nat} :
                x.natAbs % n = (x % n).toNat
                theorem Int.emod_natAbs_of_neg {x : Int} (h : x < 0) {n : Nat} (w : n 0) :
                x.natAbs % n = if n x then 0 else n - (x % n).toNat

                / and ordering #

                theorem Int.ediv_mul_le (a : Int) {b : Int} (H : b 0) :
                a / b * b a
                theorem Int.le_of_mul_le_mul_left {a b c : Int} (w : a * b a * c) (h : 0 < a) :
                b c
                theorem Int.le_of_mul_le_mul_right {a b c : Int} (w : b * a c * a) (h : 0 < a) :
                b c
                theorem Int.mul_le_mul_iff_of_pos_right {a b c : Int} (ha : 0 < a) :
                b * a c * a b c
                theorem Int.mul_nonneg_iff_of_pos_right {a b : Int} (hb : 0 < b) :
                0 a * b 0 a
                theorem Int.ediv_le_of_le_mul {a b c : Int} (H : 0 < c) (H' : a b * c) :
                a / c b
                theorem Int.ediv_nonpos_of_nonpos_of_neg {n s : Int} (h : n 0) (h2 : 0 < s) :
                n / s 0
                theorem Int.mul_lt_of_lt_ediv {a b c : Int} (H : 0 < c) (H3 : a < b / c) :
                a * c < b
                theorem Int.mul_le_of_le_ediv {a b c : Int} (H1 : 0 < c) (H2 : a b / c) :
                a * c b
                theorem Int.ediv_lt_of_lt_mul {a b c : Int} (H : 0 < c) (H' : a < b * c) :
                a / c < b
                theorem Int.lt_of_mul_lt_mul_left {a b c : Int} (w : a * b < a * c) (h : 0 a) :
                b < c
                theorem Int.lt_of_mul_lt_mul_right {a b c : Int} (w : b * a < c * a) (h : 0 a) :
                b < c
                theorem Int.le_ediv_of_mul_le {a b c : Int} (H1 : 0 < c) (H2 : a * c b) :
                a b / c
                theorem Int.le_ediv_iff_mul_le {a b c : Int} (H : 0 < c) :
                a b / c a * c b
                theorem Int.lt_mul_of_ediv_lt {a b c : Int} (H1 : 0 < c) (H2 : a / c < b) :
                a < b * c
                theorem Int.ediv_lt_iff_lt_mul {a b c : Int} (H : 0 < c) :
                a / c < b a < b * c
                theorem Int.ediv_le_iff_le_mul {k x y : Int} (h : 0 < k) :
                x / k y x < y * k + k
                theorem Int.le_mul_of_ediv_le {a b c : Int} (H1 : 0 b) (H2 : b a) (H3 : a / b c) :
                a c * b
                theorem Int.lt_ediv_of_mul_lt {a b c : Int} (H1 : 0 b) (H2 : b c) (H3 : a * b < c) :
                a < c / b
                theorem Int.lt_ediv_iff_mul_lt {a b c : Int} (H : 0 < c) (H' : c b) :
                a < b / c a * c < b
                theorem Int.ediv_pos_of_pos_of_dvd {a b : Int} (H1 : 0 < a) (H2 : 0 b) (H3 : b a) :
                0 < a / b
                theorem Int.ediv_eq_ediv_of_mul_eq_mul {a b c d : Int} (H2 : d c) (H3 : b 0) (H4 : d 0) (H5 : a * d = b * c) :
                a / b = c / d
                theorem Int.ediv_eq_iff_of_pos {k x y : Int} (h : 0 < k) :
                x / k = y y * k x x < y * k + k
                theorem Int.add_ediv_of_pos {a b c : Int} (h : 0 < c) :
                (a + b) / c = a / c + b / c + if c a % c + b % c then 1 else 0
                theorem Int.add_ediv {a b c : Int} (h : c 0) :
                (a + b) / c = a / c + b / c + if c.natAbs a % c + b % c then c.sign else 0
                theorem Int.ediv_le_ediv {a b c : Int} (H : 0 < c) (H' : a b) :
                a / c b / c
                theorem Int.not_dvd_iff_lt_mul_succ {n : Int} (m : Int) (hn : 0 < n) :
                ¬n m (k : Int), n * k < m m < n * (k + 1)

                If n > 0 then m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

                tdiv #

                @[simp]
                theorem Int.tdiv_neg (a b : Int) :
                a.tdiv (-b) = -a.tdiv b

                There are no lemmas

                @[simp]
                theorem Int.mul_tdiv_cancel (a : Int) {b : Int} (H : b 0) :
                (a * b).tdiv b = a
                @[simp]
                theorem Int.mul_tdiv_cancel_left {a : Int} (b : Int) (H : a 0) :
                (a * b).tdiv a = b
                theorem Int.tdiv_nonneg {a b : Int} (Ha : 0 a) (Hb : 0 b) :
                0 a.tdiv b
                theorem Int.tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a 0) (Hb : b 0) :
                0 a.tdiv b
                theorem Int.tdiv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) :
                a.tdiv b 0
                @[reducible, inline, deprecated Int.tdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
                abbrev Int.tdiv_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) :
                a.tdiv b 0
                Equations
                  Instances For
                    theorem Int.tdiv_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) :
                    a.tdiv b = 0
                    @[simp]
                    theorem Int.mul_tdiv_mul_of_pos {a : Int} (b c : Int) (H : 0 < a) :
                    (a * b).tdiv (a * c) = b.tdiv c
                    @[simp]
                    theorem Int.mul_tdiv_mul_of_pos_left (a : Int) {b : Int} (c : Int) (H : 0 < b) :
                    (a * b).tdiv (c * b) = a.tdiv c
                    theorem Int.tdiv_eq_of_eq_mul_right {a b c : Int} (H1 : b 0) (H2 : a = b * c) :
                    a.tdiv b = c
                    theorem Int.eq_tdiv_of_mul_eq_right {a b c : Int} (H1 : a 0) (H2 : a * b = c) :
                    b = c.tdiv a
                    theorem Int.tdiv_eq_of_eq_mul_left {a b c : Int} (H1 : b 0) (H2 : a = c * b) :
                    a.tdiv b = c
                    theorem Int.eq_tdiv_of_mul_eq_left {a b c : Int} (H1 : b 0) (H2 : a * b = c) :
                    a = c.tdiv b
                    @[simp]
                    theorem Int.tdiv_self {a : Int} (H : a 0) :
                    a.tdiv a = 1
                    @[simp]
                    theorem Int.neg_tdiv (a b : Int) :
                    (-a).tdiv b = -a.tdiv b
                    theorem Int.neg_tdiv_neg (a b : Int) :
                    (-a).tdiv (-b) = a.tdiv b
                    theorem Int.sign_tdiv (a b : Int) :
                    @[simp]
                    theorem Int.natAbs_tdiv (a b : Int) :

                    tmod #

                    theorem Int.ofNat_tmod (m n : Nat) :
                    ↑(m % n) = (↑m).tmod n
                    theorem Int.tmod_nonneg {a : Int} (b : Int) :
                    0 a0 a.tmod b
                    @[simp]
                    theorem Int.tmod_neg (a b : Int) :
                    a.tmod (-b) = a.tmod b
                    @[simp]
                    theorem Int.neg_tmod (a b : Int) :
                    (-a).tmod b = -a.tmod b
                    theorem Int.tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) :
                    a.tmod b < b
                    theorem Int.lt_tmod_of_pos (a : Int) {b : Int} (H : 0 < b) :
                    -b < a.tmod b
                    @[simp]
                    theorem Int.mul_tmod_left (a b : Int) :
                    (a * b).tmod b = 0
                    @[simp]
                    theorem Int.mul_tmod_right (a b : Int) :
                    (a * b).tmod a = 0
                    theorem Int.mul_tmod (a b n : Int) :
                    (a * b).tmod n = (a.tmod n * b.tmod n).tmod n
                    @[simp]
                    theorem Int.tmod_self {a : Int} :
                    a.tmod a = 0
                    @[simp]
                    theorem Int.tmod_tmod_of_dvd (n : Int) {m k : Int} (h : m k) :
                    (n.tmod k).tmod m = n.tmod m
                    theorem Int.tmod_tmod (a b : Int) :
                    (a.tmod b).tmod b = a.tmod b
                    theorem Int.tmod_eq_zero_of_dvd {a b : Int} :
                    a bb.tmod a = 0
                    theorem Int.tmod_eq_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) :
                    a.tmod b = a
                    theorem Int.sign_tmod (a b : Int) :
                    (a.tmod b).sign = if b a then 0 else a.sign
                    @[simp]
                    theorem Int.natAbs_tmod (a b : Int) :

                    properties of tdiv and tmod

                    theorem Int.mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) :
                    b * a.tdiv b = a
                    theorem Int.tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) :
                    a.tdiv b * b = a
                    theorem Int.dvd_of_tmod_eq_zero {a b : Int} (H : b.tmod a = 0) :
                    a b
                    theorem Int.dvd_iff_tmod_eq_zero {a b : Int} :
                    a b b.tmod a = 0
                    theorem Int.tdiv_mul_cancel {a b : Int} (H : b a) :
                    a.tdiv b * b = a
                    theorem Int.mul_tdiv_cancel' {a b : Int} (H : a b) :
                    a * b.tdiv a = b
                    theorem Int.neg_tmod_self (a : Int) :
                    (-a).tmod a = 0
                    theorem Int.lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) :
                    a < (a.tdiv b + 1) * b
                    theorem Int.mul_tdiv_assoc (a : Int) {b c : Int} :
                    c b(a * b).tdiv c = a * b.tdiv c
                    theorem Int.mul_tdiv_assoc' (b : Int) {a c : Int} (h : c a) :
                    (a * b).tdiv c = a.tdiv c * b
                    theorem Int.neg_tdiv_of_dvd {a b : Int} :
                    b a(-a).tdiv b = -a.tdiv b
                    theorem Int.tdiv_dvd_tdiv {a b c : Int} :
                    a bb cb.tdiv a c.tdiv a
                    theorem Int.mul_tdiv_cancel_of_dvd {a b : Int} (H : b a) :
                    b * a.tdiv b = a
                    theorem Int.tdiv_mul_cancel_of_dvd {a b : Int} (H : b a) :
                    a.tdiv b * b = a
                    theorem Int.tmod_two_eq (x : Int) :
                    x.tmod 2 = -1 x.tmod 2 = 0 x.tmod 2 = 1
                    theorem Int.tdiv_tmod_unique {a b r q : Int} (ha : 0 a) (hb : b 0) :
                    a.tdiv b = q a.tmod b = r r + b * q = a 0 r r < b.natAbs
                    theorem Int.tdiv_tmod_unique' {a b r q : Int} (ha : a 0) (hb : b 0) :
                    a.tdiv b = q a.tmod b = r r + b * q = a -b.natAbs < r r 0
                    @[simp]
                    theorem Int.mul_tmod_mul_of_pos {a : Int} (b c : Int) (H : 0 < a) :
                    (a * b).tmod (a * c) = a * b.tmod c
                    theorem Int.tdiv_le_self {a : Int} (b : Int) (Ha : 0 a) :
                    a.tdiv b a
                    theorem Int.dvd_tmod_sub_self {x m : Int} :
                    m x.tmod m - x
                    theorem Int.dvd_self_sub_tmod {x m : Int} :
                    m x - x.tmod m
                    theorem Int.neg_mul_tmod_right (a b : Int) :
                    (-(a * b)).tmod a = 0
                    theorem Int.neg_mul_tmod_left (a b : Int) :
                    (-(a * b)).tmod b = 0
                    @[simp]
                    theorem Int.tdiv_one (a : Int) :
                    a.tdiv 1 = a
                    @[simp]
                    theorem Int.tmod_one (a : Int) :
                    a.tmod 1 = 0
                    theorem Int.dvd_self_sub_of_tmod_eq {a b c : Int} (h : a.tmod b = c) :
                    b a - c
                    theorem Int.dvd_sub_self_of_tmod_eq {a b c : Int} (h : a.tmod b = c) :
                    b c - a
                    theorem Int.eq_mul_of_tdiv_eq_right {a b c : Int} (H1 : b a) (H2 : a.tdiv b = c) :
                    a = b * c
                    theorem Int.tdiv_eq_iff_eq_mul_right {a b c : Int} (H : b 0) (H' : b a) :
                    a.tdiv b = c a = b * c
                    theorem Int.tdiv_eq_iff_eq_mul_left {a b c : Int} (H : b 0) (H' : b a) :
                    a.tdiv b = c a = c * b
                    theorem Int.eq_mul_of_tdiv_eq_left {a b c : Int} (H1 : b a) (H2 : a.tdiv b = c) :
                    a = c * b
                    theorem Int.eq_zero_of_tdiv_eq_zero {d n : Int} (h : d n) (H : n.tdiv d = 0) :
                    n = 0
                    @[simp]
                    theorem Int.tdiv_left_inj {a b d : Int} (hda : d a) (hdb : d b) :
                    a.tdiv d = b.tdiv d a = b
                    theorem Int.tdiv_sign (a b : Int) :
                    a.tdiv b.sign = a * b.sign
                    @[simp]
                    theorem Int.mul_le_mul_left {a b c : Int} (ha : 0 < a) :
                    a * b a * c b c
                    @[simp]
                    theorem Int.mul_le_mul_right {a b c : Int} (ha : 0 < a) :
                    b * a c * a b c
                    @[simp]
                    theorem Int.mul_lt_mul_left {a b c : Int} (ha : 0 < a) :
                    a * b < a * c b < c
                    @[simp]
                    theorem Int.mul_lt_mul_right {a b c : Int} (ha : 0 < a) :
                    b * a < c * a b < c
                    @[simp]
                    theorem Int.mul_le_mul_left_of_neg {a b c : Int} (ha : a < 0) :
                    a * b a * c c b
                    @[simp]
                    theorem Int.mul_le_mul_right_of_neg {a b c : Int} (ha : a < 0) :
                    b * a c * a c b
                    @[simp]
                    theorem Int.mul_lt_mul_left_of_neg {a b c : Int} (ha : a < 0) :
                    a * b < a * c c < b
                    @[simp]
                    theorem Int.mul_lt_mul_right_of_neg {a b c : Int} (ha : a < 0) :
                    b * a < c * a c < b
                    theorem Int.ediv_le_iff_of_dvd_of_pos {a b c : Int} (hb : 0 < b) (hba : b a) :
                    a / b c a b * c
                    theorem Int.ediv_le_iff_of_dvd_of_neg {a b c : Int} (hb : b < 0) (hba : b a) :
                    a / b c b * c a
                    theorem Int.ediv_lt_iff_of_dvd_of_pos {a b c : Int} (hb : 0 < b) (hba : b a) :
                    a / b < c a < b * c
                    theorem Int.ediv_lt_iff_of_dvd_of_neg {a b c : Int} (hb : b < 0) (hba : b a) :
                    a / b < c b * c < a
                    theorem Int.le_ediv_iff_of_dvd_of_pos {a b c : Int} (hc : 0 < c) (hcb : c b) :
                    a b / c c * a b
                    theorem Int.le_ediv_iff_of_dvd_of_neg {a b c : Int} (hc : c < 0) (hcb : c b) :
                    a b / c b c * a
                    theorem Int.lt_ediv_iff_of_dvd_of_pos {a b c : Int} (hc : 0 < c) (hcb : c b) :
                    a < b / c c * a < b
                    theorem Int.lt_ediv_iff_of_dvd_of_neg {a b c : Int} (hc : c < 0) (hcb : c b) :
                    a < b / c b < c * a
                    theorem Int.ediv_le_ediv_iff_of_dvd_of_pos_of_pos {a b c d : Int} (hb : 0 < b) (hd : 0 < d) (hba : b a) (hdc : d c) :
                    a / b c / d d * a c * b
                    theorem Int.ediv_le_ediv_iff_of_dvd_of_pos_of_neg {a b c d : Int} (hb : 0 < b) (hd : d < 0) (hba : b a) (hdc : d c) :
                    a / b c / d c * b d * a
                    theorem Int.ediv_le_ediv_iff_of_dvd_of_neg_of_pos {a b c d : Int} (hb : b < 0) (hd : 0 < d) (hba : b a) (hdc : d c) :
                    a / b c / d c * b d * a
                    theorem Int.ediv_le_ediv_iff_of_dvd_of_neg_of_neg {a b c d : Int} (hb : b < 0) (hd : d < 0) (hba : b a) (hdc : d c) :
                    a / b c / d d * a c * b
                    theorem Int.ediv_lt_ediv_iff_of_dvd_of_pos {a b c d : Int} (hb : 0 < b) (hd : 0 < d) (hba : b a) (hdc : d c) :
                    a / b < c / d d * a < c * b
                    theorem Int.ediv_lt_ediv_iff_of_dvd_of_pos_of_neg {a b c d : Int} (hb : 0 < b) (hd : d < 0) (hba : b a) (hdc : d c) :
                    a / b < c / d c * b < d * a
                    theorem Int.ediv_lt_ediv_iff_of_dvd_of_neg_of_pos {a b c d : Int} (hb : b < 0) (hd : 0 < d) (hba : b a) (hdc : d c) :
                    a / b < c / d c * b < d * a
                    theorem Int.ediv_lt_ediv_iff_of_dvd_of_neg_of_neg {a b c d : Int} (hb : b < 0) (hd : d < 0) (hba : b a) (hdc : d c) :
                    a / b < c / d d * a < c * b

                    tdiv and ordering #

                    theorem Int.mul_tdiv_self_le {x k : Int} (h : 0 x) :
                    k * x.tdiv k x
                    theorem Int.lt_mul_tdiv_self_add {x k : Int} (h : 0 < k) :
                    x < k * x.tdiv k + k
                    theorem Int.tdiv_mul_le (a : Int) {b : Int} (hb : b 0) :
                    a.tdiv b * b a + ↑(if 0 a then 0 else b.natAbs - 1)
                    theorem Int.tdiv_le_of_le_mul {a b c : Int} (Hc : 0 < c) (H' : a b * c) :
                    a.tdiv c b + if 0 a then 0 else 1
                    theorem Int.le_tdiv_of_mul_le {a b c : Int} (H1 : 0 < c) (H2 : a * c b) :
                    a b.tdiv c
                    theorem Int.lt_mul_of_tdiv_lt {a b c : Int} (H1 : 0 < c) (H2 : a.tdiv c < b) :
                    a < b * c
                    theorem Int.le_mul_of_tdiv_le {a b c : Int} (H1 : 0 b) (H2 : b a) (H3 : a.tdiv b c) :
                    a c * b
                    theorem Int.lt_tdiv_of_mul_lt {a b c : Int} (H1 : 0 b) (H2 : b c) (H3 : a * b < c) :
                    a < c.tdiv b
                    theorem Int.tdiv_pos_of_pos_of_dvd {a b : Int} (H1 : 0 < a) (H2 : 0 b) (H3 : b a) :
                    0 < a.tdiv b
                    theorem Int.tdiv_eq_tdiv_of_mul_eq_mul {a b c d : Int} (H2 : d c) (H3 : b 0) (H4 : d 0) (H5 : a * d = b * c) :
                    a.tdiv b = c.tdiv d
                    theorem Int.le_emod_self_add_one_iff {a b : Int} (h : 0 < b) :
                    b a % b + 1 b a + 1
                    @[deprecated Int.le_emod_self_add_one_iff (since := "2025-04-12")]
                    theorem Int.le_mod_self_add_one_iff {a b : Int} (h : 0 < b) :
                    b a % b + 1 b a + 1
                    theorem Int.add_one_tdiv_of_pos {a b : Int} (h : 0 < b) :
                    (a + 1).tdiv b = a.tdiv b + if 0 < a + 1 b a + 1 a < 0 b a then 1 else 0
                    theorem Int.add_one_tdiv {a b : Int} :
                    (a + 1).tdiv b = a.tdiv b + if 0 < a + 1 b a + 1 a < 0 b a then b.sign else 0
                    theorem Int.tdiv_le_tdiv {a b c : Int} (H : 0 < c) (H' : a b) :
                    a.tdiv c b.tdiv c

                    fdiv #

                    theorem Int.add_mul_fdiv_right (a b : Int) {c : Int} (H : c 0) :
                    (a + b * c).fdiv c = a.fdiv c + b
                    theorem Int.add_mul_fdiv_left (a : Int) {b : Int} (c : Int) (H : b 0) :
                    (a + b * c).fdiv b = a.fdiv b + c
                    theorem Int.mul_add_fdiv_right (a c : Int) {b : Int} (H : b 0) :
                    (a * b + c).fdiv b = c.fdiv b + a
                    theorem Int.mul_add_fdiv_left (b : Int) {a : Int} (c : Int) (H : a 0) :
                    (a * b + c).fdiv a = c.fdiv a + b
                    theorem Int.sub_mul_fdiv_right (a b : Int) {c : Int} (H : c 0) :
                    (a - b * c).fdiv c = a.fdiv c - b
                    theorem Int.sub_mul_fdiv_left (a : Int) {b : Int} (c : Int) (H : b 0) :
                    (a - b * c).fdiv b = a.fdiv b - c
                    theorem Int.mul_sub_fdiv_right (a c : Int) {b : Int} (H : b 0) :
                    (a * b - c).fdiv b = a + (-c).fdiv b
                    theorem Int.mul_sub_fdiv_left (b : Int) {a : Int} (c : Int) (H : a 0) :
                    (a * b - c).fdiv a = b + (-c).fdiv a
                    @[simp]
                    theorem Int.mul_fdiv_cancel (a : Int) {b : Int} (H : b 0) :
                    (a * b).fdiv b = a
                    @[simp]
                    theorem Int.mul_fdiv_cancel_left {a : Int} (b : Int) (H : a 0) :
                    (a * b).fdiv a = b
                    theorem Int.add_fdiv_of_dvd_right {a b c : Int} (H : c b) :
                    (a + b).fdiv c = a.fdiv c + b.fdiv c
                    theorem Int.add_fdiv_of_dvd_left {a b c : Int} (H : c a) :
                    (a + b).fdiv c = a.fdiv c + b.fdiv c
                    theorem Int.fdiv_nonneg {a b : Int} (Ha : 0 a) (Hb : 0 b) :
                    0 a.fdiv b
                    theorem Int.fdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a 0) (Hb : b 0) :
                    0 a.fdiv b
                    theorem Int.fdiv_nonpos_of_nonneg_of_nonpos {a b : Int} :
                    0 ab 0a.fdiv b 0
                    @[reducible, inline, deprecated Int.fdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
                    abbrev Int.fdiv_nonpos {a b : Int} :
                    0 ab 0a.fdiv b 0
                    Equations
                      Instances For
                        theorem Int.fdiv_neg_of_neg_of_pos {a b : Int} :
                        a < 00 < ba.fdiv b < 0
                        theorem Int.fdiv_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) :
                        a.fdiv b = 0
                        @[simp]
                        theorem Int.mul_fdiv_mul_of_pos {a : Int} (b c : Int) (H : 0 < a) :
                        (a * b).fdiv (a * c) = b.fdiv c
                        @[simp]
                        theorem Int.mul_fdiv_mul_of_pos_left (a : Int) {b : Int} (c : Int) (H : 0 < b) :
                        (a * b).fdiv (c * b) = a.fdiv c
                        @[simp]
                        theorem Int.fdiv_one (a : Int) :
                        a.fdiv 1 = a
                        theorem Int.fdiv_eq_of_eq_mul_right {a b c : Int} (H1 : b 0) (H2 : a = b * c) :
                        a.fdiv b = c
                        theorem Int.eq_fdiv_of_mul_eq_right {a b c : Int} (H1 : a 0) (H2 : a * b = c) :
                        b = c.tdiv a
                        theorem Int.fdiv_eq_of_eq_mul_left {a b c : Int} (H1 : b 0) (H2 : a = c * b) :
                        a.fdiv b = c
                        theorem Int.eq_fdiv_of_mul_eq_left {a b c : Int} (H1 : b 0) (H2 : a * b = c) :
                        a = c.fdiv b
                        @[simp]
                        theorem Int.fdiv_self {a : Int} (H : a 0) :
                        a.fdiv a = 1
                        theorem Int.neg_fdiv {a b : Int} :
                        (-a).fdiv b = -a.fdiv b - if b = 0 b a then 0 else 1
                        @[simp]
                        theorem Int.neg_fdiv_neg (a b : Int) :
                        (-a).fdiv (-b) = a.fdiv b
                        theorem Int.fdiv_neg {a b : Int} (h : b 0) :
                        a.fdiv (-b) = if b a then -a.fdiv b else -a.fdiv b - 1

                        One could prove the following, but as the statements are quite awkward, so far it doesn't seem worthwhile.

                        theorem natAbs_fdiv {a b : Int} (h : b ≠ 0) :
                            natAbs (a.fdiv b) = a.natAbs / b.natAbs + if a.sign = b.sign ∨ b ∣ a then 0 else 1 := ...
                        
                        theorem sign_fdiv (a b : Int) :
                            sign (a.fdiv b) = if a.sign = b.sign ∧ natAbs a < natAbs b then 0 else sign a * sign b := ...
                        

                        fmod #

                        theorem Int.ofNat_fmod (m n : Nat) :
                        ↑(m % n) = (↑m).fmod n
                        theorem Int.fmod_nonneg {a b : Int} (ha : 0 a) (hb : 0 b) :
                        0 a.fmod b
                        theorem Int.fmod_nonneg_of_pos (a : Int) {b : Int} (hb : 0 < b) :
                        0 a.fmod b
                        @[reducible, inline, deprecated Int.fmod_nonneg_of_pos (since := "2025-03-04")]
                        abbrev Int.fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) :
                        0 a.fmod b
                        Equations
                          Instances For
                            theorem Int.fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) :
                            a.fmod b < b
                            @[simp]
                            theorem Int.add_mul_fmod_self_right (a b c : Int) :
                            (a + b * c).fmod c = a.fmod c
                            @[deprecated Int.add_mul_fmod_self_right (since := "2025-04-11")]
                            theorem Int.add_mul_fmod_self {a b c : Int} :
                            (a + b * c).fmod c = a.fmod c
                            @[simp]
                            theorem Int.add_mul_fmod_self_left (a b c : Int) :
                            (a + b * c).fmod b = a.fmod b
                            @[simp]
                            theorem Int.mul_add_fmod_self_right (a b c : Int) :
                            (a * b + c).fmod b = c.fmod b
                            @[simp]
                            theorem Int.mul_add_fmod_self_left (a b c : Int) :
                            (a * b + c).fmod a = c.fmod a
                            @[simp]
                            theorem Int.add_neg_mul_fmod_self_right (a b c : Int) :
                            (a + -(b * c)).fmod c = a.fmod c
                            @[simp]
                            theorem Int.add_neg_mul_fmod_self_left (a b c : Int) :
                            (a + -(b * c)).fmod b = a.fmod b
                            @[simp]
                            theorem Int.add_fmod_right (a b : Int) :
                            (a + b).fmod b = a.fmod b
                            @[simp]
                            theorem Int.add_fmod_left (a b : Int) :
                            (a + b).fmod a = b.fmod a
                            @[simp]
                            theorem Int.sub_mul_fmod_self_right (a b c : Int) :
                            (a - b * c).fmod c = a.fmod c
                            @[simp]
                            theorem Int.sub_mul_fmod_self_left (a b c : Int) :
                            (a - b * c).fmod b = a.fmod b
                            @[simp]
                            theorem Int.mul_sub_fmod_self_right (a b c : Int) :
                            (a * b - c).fmod b = (-c).fmod b
                            @[simp]
                            theorem Int.mul_sub_fmod_self_left (a b c : Int) :
                            (a * b - c).fmod a = (-c).fmod a
                            @[simp]
                            theorem Int.sub_fmod_right (a b : Int) :
                            (a - b).fmod b = a.fmod b
                            @[simp]
                            theorem Int.sub_fmod_left (a b : Int) :
                            (a - b).fmod a = (-b).fmod a
                            @[simp]
                            theorem Int.fmod_add_fmod (m n k : Int) :
                            (m.fmod n + k).fmod n = (m + k).fmod n
                            @[simp]
                            theorem Int.add_fmod_fmod (m n k : Int) :
                            (m + n.fmod k).fmod k = (m + n).fmod k
                            theorem Int.add_fmod (a b n : Int) :
                            (a + b).fmod n = (a.fmod n + b.fmod n).fmod n
                            theorem Int.add_fmod_eq_add_fmod_right {m n k : Int} (i : Int) (H : m.fmod n = k.fmod n) :
                            (m + i).fmod n = (k + i).fmod n
                            theorem Int.fmod_add_cancel_right {m n k : Int} (i : Int) :
                            (m + i).fmod n = (k + i).fmod n m.fmod n = k.fmod n
                            @[simp]
                            theorem Int.mul_fmod_left (a b : Int) :
                            (a * b).fmod b = 0
                            @[simp]
                            theorem Int.mul_fmod_right (a b : Int) :
                            (a * b).fmod a = 0
                            theorem Int.mul_fmod (a b n : Int) :
                            (a * b).fmod n = (a.fmod n * b.fmod n).fmod n
                            @[simp]
                            theorem Int.fmod_self {a : Int} :
                            a.fmod a = 0
                            @[simp]
                            theorem Int.fmod_fmod_of_dvd (n : Int) {m k : Int} (h : m k) :
                            (n.fmod k).fmod m = n.fmod m
                            theorem Int.fmod_fmod (a b : Int) :
                            (a.fmod b).fmod b = a.fmod b
                            theorem Int.sub_fmod (a b n : Int) :
                            (a - b).fmod n = (a.fmod n - b.fmod n).fmod n
                            theorem Int.fmod_eq_zero_of_dvd {a b : Int} :
                            a bb.fmod a = 0
                            theorem Int.fmod_eq_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) :
                            a.fmod b = a
                            @[simp]
                            theorem Int.neg_fmod_neg (a b : Int) :
                            (-a).fmod (-b) = -a.fmod b

                            properties of fdiv and fmod #

                            theorem Int.mul_fdiv_cancel_of_fmod_eq_zero {a b : Int} (H : a.fmod b = 0) :
                            b * a.fdiv b = a
                            theorem Int.fdiv_mul_cancel_of_fmod_eq_zero {a b : Int} (H : a.fmod b = 0) :
                            a.fdiv b * b = a
                            theorem Int.dvd_of_fmod_eq_zero {a b : Int} (H : b.fmod a = 0) :
                            a b
                            theorem Int.dvd_iff_fmod_eq_zero {a b : Int} :
                            a b b.fmod a = 0
                            theorem Int.fdiv_mul_cancel {a b : Int} (H : b a) :
                            a.fdiv b * b = a
                            theorem Int.mul_fdiv_cancel' {a b : Int} (H : a b) :
                            a * b.fdiv a = b
                            theorem Int.eq_mul_of_fdiv_eq_right {a b c : Int} (H1 : b a) (H2 : a.fdiv b = c) :
                            a = b * c
                            @[simp]
                            theorem Int.neg_fmod_self (a : Int) :
                            (-a).fmod a = 0
                            theorem Int.lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) :
                            a < (a.fdiv b + 1) * b
                            theorem Int.fdiv_eq_iff_eq_mul_right {a b c : Int} (H : b 0) (H' : b a) :
                            a.fdiv b = c a = b * c
                            theorem Int.fdiv_eq_iff_eq_mul_left {a b c : Int} (H : b 0) (H' : b a) :
                            a.fdiv b = c a = c * b
                            theorem Int.eq_mul_of_fdiv_eq_left {a b c : Int} (H1 : b a) (H2 : a.fdiv b = c) :
                            a = c * b
                            theorem Int.eq_zero_of_fdiv_eq_zero {d n : Int} (h : d n) (H : n.fdiv d = 0) :
                            n = 0
                            @[simp]
                            theorem Int.fdiv_left_inj {a b d : Int} (hda : d a) (hdb : d b) :
                            a.fdiv d = b.fdiv d a = b
                            theorem Int.mul_fdiv_assoc (a : Int) {b c : Int} :
                            c b(a * b).fdiv c = a * b.fdiv c
                            theorem Int.mul_fdiv_assoc' (b : Int) {a c : Int} (h : c a) :
                            (a * b).fdiv c = a.fdiv c * b
                            theorem Int.neg_fdiv_of_dvd {a b : Int} :
                            b a(-a).fdiv b = -a.fdiv b
                            theorem Int.sub_fdiv_of_dvd (a : Int) {b c : Int} (hcb : c b) :
                            (a - b).fdiv c = a.fdiv c - b.fdiv c
                            theorem Int.fdiv_dvd_fdiv {a b c : Int} :
                            a bb cb.fdiv a c.fdiv a
                            theorem Int.mul_fdiv_cancel_of_dvd {a b : Int} (H : b a) :
                            b * a.fdiv b = a
                            theorem Int.fdiv_mul_cancel_of_dvd {a b : Int} (H : b a) :
                            a.fdiv b * b = a
                            theorem Int.fmod_two_eq (x : Int) :
                            x.fmod 2 = 0 x.fmod 2 = 1
                            theorem Int.add_fmod_eq_add_fmod_left {m n k : Int} (i : Int) (H : m.fmod n = k.fmod n) :
                            (i + m).fmod n = (i + k).fmod n
                            theorem Int.fmod_add_cancel_left {m n k i : Int} :
                            (i + m).fmod n = (i + k).fmod n m.fmod n = k.fmod n
                            theorem Int.fmod_sub_cancel_right {m n k : Int} (i : Int) :
                            (m - i).fmod n = (k - i).fmod n m.fmod n = k.fmod n
                            theorem Int.fmod_eq_fmod_iff_fmod_sub_eq_zero {m n k : Int} :
                            m.fmod n = k.fmod n (m - k).fmod n = 0
                            theorem Int.fmod_sub_cancel_left {m n k : Int} (i : Int) :
                            (i - m).fmod n = (i - k).fmod n m.fmod n = k.fmod n
                            theorem Int.fdiv_fmod_unique {a b r q : Int} (h : 0 < b) :
                            a.fdiv b = q a.fmod b = r r + b * q = a 0 r r < b
                            theorem Int.fdiv_fmod_unique' {a b r q : Int} (h : b < 0) :
                            a.fdiv b = q a.fmod b = r r + b * q = a b < r r 0
                            @[simp]
                            theorem Int.mul_fmod_mul_of_pos {a : Int} (b c : Int) (H : 0 < a) :
                            (a * b).fmod (a * c) = a * b.fmod c
                            theorem Int.fdiv_le_self {a : Int} (b : Int) (Ha : 0 a) :
                            a.fdiv b a
                            theorem Int.dvd_fmod_sub_self {x m : Int} :
                            m x.fmod m - x
                            theorem Int.dvd_self_sub_fmod {x m : Int} :
                            m x - x.fmod m
                            theorem Int.dvd_self_sub_of_fmod_eq {a b c : Int} (h : a.fmod b = c) :
                            b a - c
                            theorem Int.dvd_sub_self_of_fmod_eq {a b c : Int} (h : a.fmod b = c) :
                            b c - a
                            @[simp]
                            theorem Int.neg_mul_fmod_right (a b : Int) :
                            (-(a * b)).fmod a = 0
                            @[simp]
                            theorem Int.neg_mul_fmod_left (a b : Int) :
                            (-(a * b)).fmod b = 0
                            @[simp]
                            theorem Int.fmod_one (a : Int) :
                            a.fmod 1 = 0
                            @[deprecated Int.sub_fmod_right (since := "2025-04-12")]
                            theorem Int.fmod_sub_cancel (x y : Int) :
                            (x - y).fmod y = x.fmod y
                            @[simp]
                            theorem Int.add_neg_fmod_self (a b : Int) :
                            (a + -b).fmod b = a.fmod b
                            @[simp]
                            theorem Int.neg_add_fmod_self (a b : Int) :
                            (-a + b).fmod a = b.fmod a
                            @[deprecated Int.dvd_self_sub_of_fmod_eq (since := "2025-04-12")]
                            theorem Int.dvd_sub_of_fmod_eq {a b c : Int} (h : a.fmod b = c) :
                            b a - c
                            theorem Int.fdiv_sign {a b : Int} :
                            a.fdiv b.sign = a * b.sign

                            fdiv and ordering #

                            theorem Int.mul_fdiv_self_le {x k : Int} (h : 0 < k) :
                            k * x.fdiv k x
                            theorem Int.lt_mul_fdiv_self_add {x k : Int} (h : 0 < k) :
                            x < k * x.fdiv k + k

                            bmod #

                            @[simp]
                            theorem Int.emod_bmod (x : Int) (n : Nat) :
                            (x % n).bmod n = x.bmod n
                            @[deprecated Int.emod_bmod (since := "2025-04-11")]
                            theorem Int.emod_bmod_congr (x : Int) (n : Nat) :
                            (x % n).bmod n = x.bmod n
                            theorem Int.bdiv_add_bmod (x : Int) (m : Nat) :
                            m * x.bdiv m + x.bmod m = x
                            theorem Int.bmod_add_bdiv (x : Int) (m : Nat) :
                            x.bmod m + m * x.bdiv m = x
                            theorem Int.bdiv_add_bmod' (x : Int) (m : Nat) :
                            x.bdiv m * m + x.bmod m = x
                            theorem Int.bmod_add_bdiv' (x : Int) (m : Nat) :
                            x.bmod m + x.bdiv m * m = x
                            theorem Int.bmod_eq_self_sub_mul_bdiv (x : Int) (m : Nat) :
                            x.bmod m = x - m * x.bdiv m
                            theorem Int.bmod_eq_self_sub_bdiv_mul (x : Int) (m : Nat) :
                            x.bmod m = x - x.bdiv m * m
                            theorem Int.bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) :
                            x.bmod m = x % m
                            theorem Int.bmod_neg (x : Int) (m : Nat) (p : x % m (m + 1) / 2) :
                            x.bmod m = x % m - m
                            theorem Int.bmod_eq_emod (x : Int) (m : Nat) :
                            x.bmod m = x % m - ↑(if x % m (m + 1) / 2 then m else 0)
                            @[simp]
                            theorem Int.bmod_one (x : Int) :
                            x.bmod 1 = 0
                            @[reducible, inline, deprecated Int.bmod_one (since := "2025-04-10")]
                            abbrev Int.bmod_one_is_zero (x : Int) :
                            x.bmod 1 = 0
                            Equations
                              Instances For
                                @[simp]
                                theorem Int.add_bmod_right (a : Int) (b : Nat) :
                                (a + b).bmod b = a.bmod b
                                @[simp]
                                theorem Int.add_bmod_left (a : Nat) (b : Int) :
                                (a + b).bmod a = b.bmod a
                                @[simp]
                                theorem Int.add_mul_bmod_self_right (a b : Int) (c : Nat) :
                                (a + b * c).bmod c = a.bmod c
                                @[simp]
                                theorem Int.add_mul_bmod_self_left (a : Int) (b : Nat) (c : Int) :
                                (a + b * c).bmod b = a.bmod b
                                @[simp]
                                theorem Int.mul_add_bmod_self_right (a : Int) (b : Nat) (c : Int) :
                                (a * b + c).bmod b = c.bmod b
                                @[simp]
                                theorem Int.mul_add_bmod_self_left (a : Nat) (b c : Int) :
                                (a * b + c).bmod a = c.bmod a
                                @[simp]
                                theorem Int.sub_bmod_right (a : Int) (b : Nat) :
                                (a - b).bmod b = a.bmod b
                                @[simp]
                                theorem Int.sub_bmod_left (a : Nat) (b : Int) :
                                (a - b).bmod a = (-b).bmod a
                                @[simp]
                                theorem Int.sub_mul_bmod_self_right (a b : Int) (c : Nat) :
                                (a - b * c).bmod c = a.bmod c
                                @[simp]
                                theorem Int.sub_mul_bmod_self_left (a : Int) (b : Nat) (c : Int) :
                                (a - b * c).bmod b = a.bmod b
                                @[simp]
                                theorem Int.mul_sub_bmod_self_right (a : Int) (b : Nat) (c : Int) :
                                (a * b - c).bmod b = (-c).bmod b
                                @[simp]
                                theorem Int.mul_sub_bmod_self_left (a : Nat) (b c : Int) :
                                (a * b - c).bmod a = (-c).bmod a
                                @[simp]
                                theorem Int.add_neg_mul_bmod_self_right (a b : Int) (c : Nat) :
                                (a + -(b * c)).bmod c = a.bmod c
                                @[simp]
                                theorem Int.add_neg_mul_bmod_self_left (a : Int) (b : Nat) (c : Int) :
                                (a + -(b * c)).bmod b = a.bmod b
                                @[deprecated Int.add_bmod_right (since := "2025-04-10")]
                                theorem Int.bmod_add_cancel {x : Int} {n : Nat} :
                                (x + n).bmod n = x.bmod n
                                @[deprecated Int.add_mul_bmod_self_left (since := "2025-04-10")]
                                theorem Int.bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) :
                                (x + n * k).bmod n = x.bmod n
                                @[deprecated Int.sub_bmod_right (since := "2025-04-10")]
                                theorem Int.bmod_sub_cancel (x : Int) (n : Nat) :
                                (x - n).bmod n = x.bmod n
                                @[deprecated Int.sub_mul_bmod_self_left (since := "2025-04-10")]
                                theorem Int.Int.bmod_sub_mul_cancel (x : Int) (n : Nat) (k : Int) :
                                (x - n * k).bmod n = x.bmod n
                                @[simp]
                                theorem Int.emod_add_bmod {y : Int} (x : Int) (n : Nat) :
                                (x % n + y).bmod n = (x + y).bmod n
                                @[deprecated Int.emod_add_bmod (since := "2025-04-11")]
                                theorem Int.emod_add_bmod_congr {y : Int} (x : Int) (n : Nat) :
                                (x % n + y).bmod n = (x + y).bmod n
                                @[simp]
                                theorem Int.emod_sub_bmod {y : Int} (x : Int) (n : Nat) :
                                (x % n - y).bmod n = (x - y).bmod n
                                @[deprecated Int.emod_sub_bmod (since := "2025-04-11")]
                                theorem Int.emod_sub_bmod_congr {y : Int} (x : Int) (n : Nat) :
                                (x % n - y).bmod n = (x - y).bmod n
                                @[simp]
                                theorem Int.sub_emod_bmod {y : Int} (x : Int) (n : Nat) :
                                (x - y % n).bmod n = (x - y).bmod n
                                @[deprecated Int.sub_emod_bmod (since := "2025-04-11")]
                                theorem Int.sub_emod_bmod_congr {y : Int} (x : Int) (n : Nat) :
                                (x - y % n).bmod n = (x - y).bmod n
                                @[simp]
                                theorem Int.emod_mul_bmod {y : Int} (x : Int) (n : Nat) :
                                (x % n * y).bmod n = (x * y).bmod n
                                @[deprecated Int.emod_mul_bmod (since := "2025-04-11")]
                                theorem Int.emod_mul_bmod_congr {y : Int} (x : Int) (n : Nat) :
                                (x % n * y).bmod n = (x * y).bmod n
                                @[simp]
                                theorem Int.bmod_add_bmod {x : Int} {n : Nat} {y : Int} :
                                (x.bmod n + y).bmod n = (x + y).bmod n
                                @[deprecated Int.bmod_add_bmod (since := "2025-04-11")]
                                theorem Int.bmod_add_bmod_congr {x : Int} {n : Nat} {y : Int} :
                                (x.bmod n + y).bmod n = (x + y).bmod n
                                @[simp]
                                theorem Int.bmod_sub_bmod {x : Int} {n : Nat} {y : Int} :
                                (x.bmod n - y).bmod n = (x - y).bmod n
                                @[deprecated Int.bmod_sub_bmod (since := "2025-04-11")]
                                theorem Int.bmod_sub_bmod_congr {x : Int} {n : Nat} {y : Int} :
                                (x.bmod n - y).bmod n = (x - y).bmod n
                                theorem Int.add_bmod_eq_add_bmod_right {x : Int} {n : Nat} {y : Int} (i : Int) (H : x.bmod n = y.bmod n) :
                                (x + i).bmod n = (y + i).bmod n
                                theorem Int.bmod_add_cancel_right {x : Int} {n : Nat} {y : Int} (i : Int) :
                                (x + i).bmod n = (y + i).bmod n x.bmod n = y.bmod n
                                theorem Int.bmod_add_cancel_left {x : Int} {n : Nat} {y : Int} (i : Int) :
                                (i + x).bmod n = (i + y).bmod n x.bmod n = y.bmod n
                                theorem Int.add_bmod_eq_add_bmod_left {x : Int} {n : Nat} {y : Int} (i : Int) (h : x.bmod n = y.bmod n) :
                                (i + x).bmod n = (i + y).bmod n
                                @[simp]
                                theorem Int.add_bmod_bmod {x y : Int} {n : Nat} :
                                (x + y.bmod n).bmod n = (x + y).bmod n
                                @[simp]
                                theorem Int.sub_bmod_bmod {x y : Int} {n : Nat} :
                                (x - y.bmod n).bmod n = (x - y).bmod n
                                @[simp]
                                theorem Int.bmod_mul_bmod {x : Int} {n : Nat} {y : Int} :
                                (x.bmod n * y).bmod n = (x * y).bmod n
                                @[simp]
                                theorem Int.mul_bmod_bmod {x y : Int} {n : Nat} :
                                (x * y.bmod n).bmod n = (x * y).bmod n
                                @[simp]
                                theorem Int.add_emod_bmod {y : Int} (x : Int) (n : Nat) :
                                (y + x % n).bmod n = (y + x).bmod n
                                @[simp]
                                theorem Int.mul_emod_bmod {y : Int} (x : Int) (n : Nat) :
                                (y * (x % n)).bmod n = (y * x).bmod n
                                @[simp]
                                theorem Int.mul_bmod_left (a : Int) (b : Nat) :
                                (a * b).bmod b = 0
                                @[simp]
                                theorem Int.mul_bmod_right (a : Nat) (b : Int) :
                                (a * b).bmod a = 0
                                theorem Int.mul_bmod (a b : Int) (n : Nat) :
                                (a * b).bmod n = (a.bmod n * b.bmod n).bmod n
                                theorem Int.add_bmod (a b : Int) (n : Nat) :
                                (a + b).bmod n = (a.bmod n + b.bmod n).bmod n
                                theorem Int.sub_bmod (a b : Int) (n : Nat) :
                                (a - b).bmod n = (a.bmod n - b.bmod n).bmod n
                                @[simp]
                                theorem Int.bmod_bmod {x : Int} {m : Nat} :
                                (x.bmod m).bmod m = x.bmod m
                                @[simp]
                                theorem Int.zero_bmod {m : Nat} :
                                bmod 0 m = 0
                                @[simp]
                                theorem Int.bmod_zero {m : Int} :
                                m.bmod 0 = m
                                @[simp]
                                theorem Int.bmod_self {a : Nat} :
                                (↑a).bmod a = 0
                                @[simp]
                                theorem Int.neg_bmod_self {a : Nat} :
                                (-a).bmod a = 0
                                theorem Int.dvd_bmod_sub_self {x : Int} {m : Nat} :
                                m x.bmod m - x
                                theorem Int.dvd_self_sub_bmod {x : Int} {m : Nat} :
                                m x - x.bmod m
                                theorem Int.dvd_of_bmod_eq_zero {a : Nat} {b : Int} (h : b.bmod a = 0) :
                                a b
                                theorem Int.bmod_eq_zero_of_dvd {a : Nat} {b : Int} (h : a b) :
                                b.bmod a = 0
                                theorem Int.dvd_iff_bmod_eq_zero {a : Nat} {b : Int} :
                                a b b.bmod a = 0
                                theorem Int.divExact_eq_bdiv {a : Int} {b : Nat} (h : b a) :
                                a.divExact (↑b) h = a.bdiv b
                                theorem Int.le_bmod {x : Int} {m : Nat} (h : 0 < m) :
                                -(m / 2) x.bmod m
                                theorem Int.bmod_lt {x : Int} {m : Nat} (h : 0 < m) :
                                x.bmod m < (m + 1) / 2
                                theorem Int.bmod_eq_iff {a : Int} {b : Nat} {c : Int} (hb : 0 < b) :
                                a.bmod b = c -(b / 2) c c < (b + 1) / 2 b c - a
                                theorem Int.bmod_eq_emod_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) :
                                x.bmod m = x % m
                                theorem Int.bmod_eq_neg {n : Nat} {m : Int} (hm : 0 m) (hn : n = 2 * m) :
                                m.bmod n = -m
                                theorem Int.bmod_le {x : Int} {m : Nat} (h : 0 < m) :
                                x.bmod m (m - 1) / 2
                                theorem Int.bmod_natAbs_add_one (x : Int) (w : x -1) :
                                x.bmod (x.natAbs + 1) = -x.sign
                                @[reducible, inline, deprecated Int.bmod_natAbs_add_one (since := "2025-04-04")]
                                abbrev Int.bmod_natAbs_plus_one (x : Int) (w : x -1) :
                                x.bmod (x.natAbs + 1) = -x.sign
                                Equations
                                  Instances For
                                    theorem Int.bmod_self_add_one {x : Nat} :
                                    (↑x).bmod (x + 1) = if x = 0 then 0 else -1
                                    theorem Int.one_bmod_two :
                                    bmod 1 2 = -1
                                    theorem Int.one_bmod {b : Nat} (h : 3 b) :
                                    bmod 1 b = 1
                                    theorem Int.bmod_two_eq (x : Int) :
                                    x.bmod 2 = -1 x.bmod 2 = 0
                                    theorem Int.bmod_sub_cancel_right {x : Int} {n : Nat} {y : Int} (i : Int) :
                                    (x - i).bmod n = (y - i).bmod n x.bmod n = y.bmod n
                                    theorem Int.bmod_eq_bmod_iff_bmod_sub_eq_zero {m : Int} {n : Nat} {k : Int} :
                                    m.bmod n = k.bmod n (m - k).bmod n = 0
                                    theorem Int.bmod_sub_cancel_left {x : Int} {n : Nat} {y : Int} (i : Int) :
                                    (i - x).bmod n = (i - y).bmod n x.bmod n = y.bmod n
                                    theorem Int.mod_bmod_mul_of_pos {a : Nat} (b : Int) (c : Nat) (h : 0 < a) (hce : 2 c) :
                                    (a * b).bmod (a * c) = a * b.bmod c
                                    @[simp]
                                    theorem Int.bmod_neg_bmod {x : Int} {n : Nat} :
                                    (-x.bmod n).bmod n = (-x).bmod n
                                    theorem Int.neg_bmod {a : Int} {b : Nat} :
                                    (-a).bmod b = if b 2 * a then a.bmod b else -a.bmod b
                                    @[simp]
                                    theorem Int.neg_mul_bmod_left (a : Int) (b : Nat) :
                                    (-(a * b)).bmod b = 0
                                    @[simp]
                                    theorem Int.neg_mul_bmod_right (a : Nat) (b : Int) :
                                    (-(a * b)).bmod a = 0
                                    @[simp]
                                    theorem Int.add_neg_bmod_self (a : Int) (b : Nat) :
                                    (a + -b).bmod b = a.bmod b
                                    @[simp]
                                    theorem Int.neg_add_bmod_self (a : Nat) (b : Int) :
                                    (-a + b).bmod a = b.bmod a
                                    theorem Int.dvd_self_sub_of_bmod_eq {a : Int} {b : Nat} {c : Int} (h : a.bmod b = c) :
                                    b a - c
                                    theorem Int.dvd_sub_self_of_bmod_eq {a : Int} {b : Nat} {c : Int} (h : a.bmod b = c) :
                                    b c - a
                                    theorem Int.bmod_neg_iff {m : Nat} {x : Int} (h2 : -m x) (h1 : x < m) :
                                    x.bmod m < 0 -(m / 2) x x < 0 (m + 1) / 2 x
                                    theorem Int.bmod_eq_of_le {n : Int} {m : Nat} (hn' : -(m / 2) n) (hn : n < (m + 1) / 2) :
                                    n.bmod m = n
                                    @[deprecated Int.bmod_eq_of_le (since := "2025-04-11")]
                                    theorem Int.bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) n) (hn : n < (m + 1) / 2) :
                                    n.bmod m = n
                                    theorem Int.bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n m) :
                                    (a.bmod m).bmod n = a.bmod n
                                    theorem Int.bmod_eq_of_le_mul_two {x : Int} {y : Nat} (hle : -y x * 2) (hlt : x * 2 < y) :
                                    x.bmod y = x
                                    @[deprecated Int.bmod_eq_of_le_mul_two (since := "2025-04-11")]
                                    theorem Int.bmod_eq_self_of_le_mul_two {x : Int} {y : Nat} (hle : -y x * 2) (hlt : x * 2 < y) :
                                    x.bmod y = x
                                    theorem Int.ediv_lt_self_of_pos_of_ne_one {x y : Int} (hx : 0 < x) (hy : y 1) :
                                    x / y < x
                                    theorem Int.ediv_nonneg_of_nonneg_of_nonneg {x y : Int} (hx : 0 x) (hy : 0 y) :
                                    0 x / y
                                    theorem Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one {x y : Int} (hx : x < -1) (hy : y < -1) :
                                    x / y < x.natAbs

                                    When both x and y are negative we need stricter bounds on x and y to establish the upper bound of x/y, i.e., x / y < x.natAbs. In particular, consider the following counter examples: · (-1) / (-2) = 1 and ¬ 1 < (-1).natAbs (note that Int.neg_one_ediv already handles ediv where the numerator is -1) · (-2) / (-1) = 2 and ¬ 1 < (-2).natAbs To exclude these cases, we enforce stricter bounds on the values of x and y.

                                    theorem Int.self_le_ediv_of_nonpos_of_nonneg {x y : Int} (hx : x 0) (hy : 0 y) :
                                    x x / y
                                    theorem Int.neg_self_le_ediv_of_nonneg_of_nonpos (x y : Int) (hx : 0 x) (hy : y 0) :
                                    -x x / y

                                    Helper theorems for dvd simproc

                                    theorem Int.dvd_eq_true_of_mod_eq_zero {a b : Int} (h : (b % a == 0) = true) :
                                    (a b) = True
                                    theorem Int.dvd_eq_false_of_mod_ne_zero {a b : Int} (h : (b % a != 0) = true) :
                                    (a b) = False