-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1) = - x.sign

Proof state:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 1 + 1 = 2

Tactic:
decide

Result:
no goals

Proof state:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 1 < (1 + ↑(x + 1) + 1 + 1) / 2

Tactic:
rw [Int.add_assoc, add_ediv_of_dvd_right, show (1 + 1 : Int) = 2 by decide, Int.ediv_self]

Result:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 1 < (1 + ↑(x + 1)) / 2 + 1

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Proof state:
case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 1 ≤ (1 + ↑(x + 1)) / 2

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Tactic:
rw [Int.add_comm, ofNat_add, Int.add_assoc, add_ediv_of_dvd_right,
  show ((1 : Nat) + 1 : Int) = 2 by decide, Int.ediv_self]

Result:
case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 1 ≤ ↑x / 2 + 1

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ ↑1 + 1

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Proof state:
case ofNat
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < (ofNat x).natAbs
⊢ (ofNat x).bmod ((ofNat x).natAbs + 1) = -(ofNat x).sign

Tactic:
simp only [bmod, ofNat_eq_coe, natAbs_ofNat, natCast_add, ofNat_one,
  emod_self_add_one (ofNat_nonneg x)]

Result:
case ofNat
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < (ofNat x).natAbs
⊢ (if ↑x < (↑x + 1 + 1) / 2 then ↑x else ↑x - (↑x + 1)) = -(↑x).sign

Proof state:
x✝ : Int
w : 1 < x✝.natAbs
t₁ : ∀ (x : Nat), x % (x + 2) = x
x : Int
h : 0 ≤ x
⊢ x % (x + 2) = x

Tactic:
match x, h with
| Int.ofNat x, _ => erw [← Int.ofNat_two, ← ofNat_add, ← ofNat_emod, t₁]; rfl

Result:
no goals

Proof state:
case negSucc
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < -[x+1].natAbs
⊢ (if ↑(x + 1) + 1 - 1 - ↑x % (↑(x + 1) + 1) < (↑(x + 1) + 1 + 1) / 2 then ↑(x + 1) + 1 - 1 - ↑x % (↑(x + 1) + 1)
    else ↑(x + 1) + 1 - 1 - ↑x % (↑(x + 1) + 1) - (↑(x + 1) + 1)) =
    1

case negSucc.bpos
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < -[x+1].natAbs
⊢ 0 < ↑(x + 1) + 1

Tactic:
erw [t₂]

Result:
case negSucc
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < -[x+1].natAbs
⊢ (if ↑(x + 1) + 1 - 1 - ↑x < (↑(x + 1) + 1 + 1) / 2 then ↑(x + 1) + 1 - 1 - ↑x
    else ↑(x + 1) + 1 - 1 - ↑x - (↑(x + 1) + 1)) =
    1

case negSucc.a
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < -[x+1].natAbs
⊢ 0 ≤ ↑x

case negSucc.bpos
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < -[x+1].natAbs
⊢ 0 < ↑(x + 1) + 1

Proof state:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ x✝ x : Nat
w : 1 < (ofNat (x + 1 + 1)).natAbs
⊢ (x + 1 + 1 + 1 + 1) / 2 ≤ x + 1 + 1

Tactic:
apply Nat.div_le_of_le_mul

Result:
case a
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ x✝ x : Nat
w : 1 < (ofNat (x + 1 + 1)).natAbs
⊢ x + 1 + 1 + 1 + 1 ≤ 2 * (x + 1 + 1)

Proof state:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝ x : Nat
w : 1 < (ofNat (x + 1)).natAbs
⊢ ↑(x + 1) - (↑(x + 1) + 1) = -(↑(x + 1)).sign

Tactic:
simp [← Int.sub_sub]

Result:
no goals

Proof state:
case hnc
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝ x : Nat
w : 1 < (ofNat (x + 1)).natAbs
⊢ ↑((x + 1 + 1 + 1) / 2) ≤ ↑(x + 1)

Tactic:
match x with
| 0 => apply Int.le_refl
| (x+1) =>
  refine Int.ofNat_le.mpr ?_
  apply Nat.div_le_of_le_mul
  simp only [Nat.two_mul, Nat.add_assoc]
  apply Nat.add_le_add_left (Nat.add_le_add_left (Nat.add_le_add_left (Nat.le_add_left
    _ _) _) _)

Result:
no goals

Proof state:
case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 1 ≤ ↑x / 2 + 1

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ ↑1 + 1

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Tactic:
apply Int.le_add_of_nonneg_left

Result:
case H.h
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 0 ≤ ↑x / 2

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ ↑1 + 1

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Proof state:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ x✝ x : Nat
w : 1 < (ofNat (x + 1 + 1)).natAbs
⊢ ↑((x + 1 + 1 + 1 + 1) / 2) ≤ ↑(x + 1 + 1)

Tactic:
refine Int.ofNat_le.mpr ?_

Result:
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ x✝ x : Nat
w : 1 < (ofNat (x + 1 + 1)).natAbs
⊢ (x + 1 + 1 + 1 + 1) / 2 ≤ x + 1 + 1

Proof state:
x✝² : Int
w : 1 < x✝².natAbs
t₁ : ∀ (x : Nat), x % (x + 2) = x
x✝¹ : Int
h : 0 ≤ x✝¹
x : Nat
x✝ : 0 ≤ ofNat x
⊢ ↑x = ofNat x

Tactic:
rfl

Result:
no goals