n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
⊢ Int.natAbs (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n) = min (val a) (n - val a)
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
⊢ Int.natAbs (valMinAbs a) = min (val a) (n - val a)
rw [valMinAbs_def_pos]
case inl
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ Int.natAbs ↑(val a) = min (val a) (n - val a)

case inr
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ Int.natAbs (↑(val a) - ↑n) = min (val a) (n - val a)
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
⊢ Int.natAbs (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n) = min (val a) (n - val a)
split_ifs with h
case inl
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ val a = min (val a) (n - val a)
case inl
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ Int.natAbs ↑(val a) = min (val a) (n - val a)
rw [Int.natAbs_ofNat]
case inl
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ min (val a) (n - val a) = val a
case inl
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ val a = min (val a) (n - val a)
symm
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ n - (n - n / 2) ≤ n / 2
case inl
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ min (val a) (n - val a) = val a
apply
  min_eq_left (le_trans h (le_trans (Nat.half_le_of_sub_le_half _) (Nat.sub_le_sub_left n h)))
no goals
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ n - (n - n / 2) ≤ n / 2
rw [Nat.sub_sub_self (Nat.div_le_self _ _)]
case inr
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ Int.natAbs ↑(n - val a) = min (val a) (n - val a)
case inr
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ Int.natAbs (↑(val a) - ↑n) = min (val a) (n - val a)
rw [← Int.natAbs_neg, neg_sub, ← Nat.cast_sub a.val_le]
case inr
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ min (val a) (n - val a) = Int.natAbs ↑(n - val a)
case inr
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ Int.natAbs ↑(n - val a) = min (val a) (n - val a)
symm
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ n / 2 < n - (n - Nat.succ (n / 2))
case inr
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ min (val a) (n - val a) = Int.natAbs ↑(n - val a)
apply
  min_eq_right
    (le_trans (le_trans (Nat.sub_le_sub_left n (lt_of_not_ge h)) (Nat.le_half_of_half_lt_sub _))
      (le_of_not_ge h))
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ n / 2 < Nat.succ (n / 2)
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ n / 2 < n - (n - Nat.succ (n / 2))
rw [Nat.sub_sub_self (Nat.div_lt_self (lt_of_le_of_ne' (Nat.zero_le _) hpos.1) one_lt_two)]
no goals
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ n / 2 < Nat.succ (n / 2)
apply Nat.lt_succ_self