n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑(valMinAbs x) ∧ valMinAbs x * 2 ∈ Set.Ioc (-↑n) ↑n
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
⊢ valMinAbs x = y → x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
rintro rfl
no goals
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑(valMinAbs x) ∧ valMinAbs x * 2 ∈ Set.Ioc (-↑n) ↑n
exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ valMinAbs x - y = 0
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ valMinAbs x = y
rw [← sub_eq_zero]
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ valMinAbs x - y

case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ abs (valMinAbs x - y) < ↑n
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ valMinAbs x - y = 0
apply @Int.eq_zero_of_abs_lt_dvd n
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ abs (valMinAbs x - y) * 2 < ↑n * 2
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ abs (valMinAbs x - y) < ↑n
rw [← mul_lt_mul_right (@zero_lt_two ℤ _ _ _ _ _)]
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ abs (valMinAbs x - y) * abs 2 < ↑n * 2
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ abs (valMinAbs x - y) * 2 < ↑n * 2
nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < valMinAbs x * 2 - y * 2 ∧ valMinAbs x * 2 - y * 2 < ↑n * 2
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ abs (valMinAbs x - y) * abs 2 < ↑n * 2
rw [← abs_mul, sub_mul, abs_lt]
no goals
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < valMinAbs x * 2 - y * 2 ∧ valMinAbs x * 2 - y * 2 < ↑n * 2
constructor <;> linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]
no goals
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ valMinAbs x - y
rw [← int_cast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]