-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem le_bmod {x : Int} {m : Nat} (h : 0 < m) : - (m/2) ≤ Int.bmod x m

Proof state:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
⊢ -(↑m / 2) ≤ (↑m + 1) / 2 - ↑m

Tactic:
rw [← ediv_add_emod m 2]

Result:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
⊢ -((2 * (↑m / 2) + ↑m % 2) / 2) ≤ (2 * (↑m / 2) + ↑m % 2 + 1) / 2 - (2 * (↑m / 2) + ↑m % 2)

Proof state:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -((2 * q + 0) / 2) ≤ (2 * q + 0 + 1) / 2 - (2 * q + 0)

Tactic:
rw [Int.add_zero, Int.mul_ediv_cancel_left, Int.add_ediv_of_dvd_left,
  Int.mul_ediv_cancel_left, show (1 / 2 : Int) = 0 by decide, Int.add_zero,
  Int.neg_eq_neg_one_mul]

Result:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -1 * q ≤ q - 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Proof state:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
⊢ -(↑m / 2) ≤ x % ↑m - ↑m

Tactic:
refine Int.le_trans ?_ (Int.sub_le_sub_right w _)

Result:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
⊢ -(↑m / 2) ≤ (↑m + 1) / 2 - ↑m

Proof state:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
⊢ -((2 * (↑m / 2) + ↑m % 2) / 2) ≤ (2 * (↑m / 2) + ↑m % 2 + 1) / 2 - (2 * (↑m / 2) + ↑m % 2)

Tactic:
generalize (m : Int) / 2 = q

Result:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
⊢ -((2 * q + ↑m % 2) / 2) ≤ (2 * q + ↑m % 2 + 1) / 2 - (2 * q + ↑m % 2)

Proof state:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

Tactic:
all_goals apply Int.dvd_mul_right

Result:
no goals

Proof state:
case isTrue.refine_1
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ -(↑m / 2) ≤ 0

Tactic:
exact Int.neg_nonpos_of_nonneg (Int.ediv_nonneg (Int.ofNat_nonneg _) (by decide))

Result:
no goals

Proof state:
case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Tactic:
all_goals try decide

Result:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

Proof state:
case isFalse
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q r : Int
h : ↑m % 2 = r
v : r = 0 ∨ r = 1
⊢ -((2 * q + r) / 2) ≤ (2 * q + r + 1) / 2 - (2 * q + r)

Tactic:
rcases v with rfl | rfl

Result:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -((2 * q + 0) / 2) ≤ (2 * q + 0 + 1) / 2 - (2 * q + 0)

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -((2 * q + 1) / 2) ≤ (2 * q + 1 + 1) / 2 - (2 * q + 1)

Proof state:
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 1 + -1 = 0

Tactic:
decide

Result:
no goals

Proof state:
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ 0 ≤ 2

Tactic:
decide

Result:
no goals

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -q ≤ q + -2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
rw [Int.neg_eq_neg_one_mul]

Result:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -1 * q ≤ q + -2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Proof state:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -1 * q ≤ q - 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Tactic:
conv => rhs; congr; rw [← Int.one_mul q]

Result:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -1 * q ≤ 1 * q - 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -1 * q ≤ q + -2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
conv => rhs; congr; rw [← Int.one_mul q]

Result:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -1 * q ≤ 1 * q + -2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ -(↑m / 2) ≤ if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m

Tactic:
have v : (m : Int) % 2 = 0 ∨ (m : Int) % 2 = 1 := emod_two_eq _

Result:
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
⊢ -(↑m / 2) ≤ if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m