case zero
a : ZMod Nat.zero
⊢ valMinAbs a * 2 = ↑Nat.zero ↔ 2 * val a = Nat.zero

case succ
n : ℕ
a : ZMod (Nat.succ n)
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
n : ℕ
a : ZMod n
⊢ valMinAbs a * 2 = ↑n ↔ 2 * val a = n
cases' n with n
case pos
n : ℕ
a : ZMod (Nat.succ n)
h : val a ≤ Nat.succ n / 2
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n

case neg
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
case succ
n : ℕ
a : ZMod (Nat.succ n)
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
by_cases h : a.val ≤ n.succ / 2
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ ¬valMinAbs a * 2 = ↑(Nat.succ n)

n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ 2 * val a = Nat.succ n → val a ≤ Nat.succ n / 2
case neg
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
apply iff_of_false _ (mt _ h)
no goals
case zero
a : ZMod Nat.zero
⊢ valMinAbs a * 2 = ↑Nat.zero ↔ 2 * val a = Nat.zero
simp
case pos
n : ℕ
a : ZMod (Nat.succ n)
h : val a ≤ Nat.succ n / 2
⊢ (if val a ≤ Nat.succ n / 2 then ↑(val a) else ↑(val a) - ↑(Nat.succ n)) * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
case pos
n : ℕ
a : ZMod (Nat.succ n)
h : val a ≤ Nat.succ n / 2
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
dsimp [valMinAbs]
no goals
case pos
n : ℕ
a : ZMod (Nat.succ n)
h : val a ≤ Nat.succ n / 2
⊢ (if val a ≤ Nat.succ n / 2 then ↑(val a) else ↑(val a) - ↑(Nat.succ n)) * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
rw [if_pos h, ← Int.coe_nat_inj', Nat.cast_mul, Nat.cast_two, mul_comm]
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ False
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ ¬valMinAbs a * 2 = ↑(Nat.succ n)
intro he
n : ℕ
a : ZMod (Nat.succ n)
h✝ : ¬0 ≤ valMinAbs a
h : ¬0 ≤ ↑(Nat.succ n)
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ False

n : ℕ
a : ZMod (Nat.succ n)
h : ¬0 ≤ valMinAbs a
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ 0 < 2
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ False
rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
no goals
n : ℕ
a : ZMod (Nat.succ n)
h✝ : ¬0 ≤ valMinAbs a
h : ¬0 ≤ ↑(Nat.succ n)
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ False

n : ℕ
a : ZMod (Nat.succ n)
h : ¬0 ≤ valMinAbs a
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ 0 < 2
exacts [h (Nat.cast_nonneg _), zero_lt_two]
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ val a * 2 = Nat.succ n → val a ≤ Nat.succ n / 2
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ 2 * val a = Nat.succ n → val a ≤ Nat.succ n / 2
rw [mul_comm]
no goals
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ val a * 2 = Nat.succ n → val a ≤ Nat.succ n / 2
exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le