-- 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:
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:
simp only [← natCast_add, ← ofNat_one, ← ofNat_two, ← ofNat_ediv]

Result:
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)

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

Tactic:
rw [if_pos] <;> simp +decide

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
⊢ 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:
all_goals decide

Result:
no goals

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

Tactic:
match x, w with
| (x+1), _ =>
  rw [Int.add_assoc, add_ediv_of_dvd_right, show (1 + 1 : Int) = 2 by decide, Int.ediv_self]
  apply Int.lt_add_one_of_le
  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]
  apply Int.le_add_of_nonneg_left
  exact Int.le.intro_sub _ rfl
  all_goals 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
⊢ 2 ∣ 1 + 1

Tactic:
decide

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
⊢ -[x+1].bmod (-[x+1].natAbs + 1) = - -[x+1].sign

Tactic:
rw [bmod, natAbs_negSucc, natCast_add, ofNat_one, sign_negSucc, Int.neg_neg,
  Nat.succ_eq_add_one, negSucc_emod]

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) < (↑(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

Proof state:
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)

Tactic:
simp only [Nat.two_mul, Nat.add_assoc]

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))) ≤ x + (1 + (1 + (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
⊢ ofNat x % (ofNat x + 2) = ofNat x

Tactic:
erw [← Int.ofNat_two, ← ofNat_add, ← ofNat_emod, t₁]

Result:
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

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)) / 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

Tactic:
apply Int.lt_add_one_of_le

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 ≤ (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

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
⊢ (if ↑(x + 1) < (↑(x + 1) + 1 + 1) / 2 then ↑(x + 1) else ↑(x + 1) - (↑(x + 1) + 1)) = -(↑(x + 1)).sign

Tactic:
rw [if_neg]

Result:
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

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) < (↑(x + 1) + 1 + 1) / 2

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:
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) < (↑(x + 1) + 1 + 1) / 2

Tactic:
refine Int.not_lt.mpr ?_

Result:
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)

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 + 1) / 2 then ↑(x + 1) + 1 - 1 - ↑x
    else ↑(x + 1) + 1 - 1 - ↑x - (↑(x + 1) + 1)) =
    1

Tactic:
rw [natCast_add, ofNat_one, Int.add_sub_cancel, Int.add_comm, Int.add_sub_cancel, if_pos]

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

Proof state:
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))) ≤ x + (1 + (1 + (x + (1 + 1))))

Tactic:
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 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:
exact succ_ofNat_pos (x + 1)

Result:
no goals

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

Tactic:
apply Int.le_refl

Result:
no goals

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

Tactic:
have t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x := fun x h => by
  match x, h with
  | Int.ofNat x, _ => erw [← Int.ofNat_two, ← ofNat_add, ← ofNat_emod, t₁]; rfl

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