n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
haveI npos : NeZero n :=
  ⟨by
    rintro rfl
    simp [fact_iff] at hn⟩
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
have _hn2 : (n : ℕ) / 2 < n :=
  Nat.div_lt_of_lt_mul ((lt_mul_iff_one_lt_left <| NeZero.pos n).2 (by decide))
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
have hn2' : (n : ℕ) - n / 2 = n / 2 + 1 := by
  conv =>
    lhs
    congr
    rw [← Nat.succ_sub_one n, Nat.succ_sub <| NeZero.pos n]
  rw [← Nat.two_mul_odd_div_two hn.1, two_mul, ← Nat.succ_add, add_tsub_cancel_right]
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
hxn : n - val x < n
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
have hxn : (n : ℕ) - x.val < n := by
  rw [tsub_lt_iff_tsub_lt x.val_le le_rfl, tsub_self]
  rw [← ZMod.nat_cast_zmod_val x] at hx0
  exact Nat.pos_of_ne_zero fun h => by simp [h] at hx0
hn : Fact (0 % 2 = 1)
x : ZMod 0
hx0 : x ≠ 0
⊢ False
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
⊢ n ≠ 0
rintro rfl
no goals
hn : Fact (0 % 2 = 1)
x : ZMod 0
hx0 : x ≠ 0
⊢ False
simp [fact_iff] at hn
no goals
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
⊢ 1 < 2
decide
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
⊢ Nat.succ (n - Nat.succ 0) - n / 2 = n / 2 + 1
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
⊢ n - n / 2 = n / 2 + 1
conv =>
  lhs
  congr
  rw [← Nat.succ_sub_one n, Nat.succ_sub <| NeZero.pos n]
no goals
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
⊢ Nat.succ (n - Nat.succ 0) - n / 2 = n / 2 + 1
rw [← Nat.two_mul_odd_div_two hn.1, two_mul, ← Nat.succ_add, add_tsub_cancel_right]
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ 0 < val x
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ n - val x < n
rw [tsub_lt_iff_tsub_lt x.val_le le_rfl, tsub_self]
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : ↑(val x) ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ 0 < val x
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ 0 < val x
rw [← ZMod.nat_cast_zmod_val x] at hx0
no goals
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : ↑(val x) ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
⊢ 0 < val x
exact Nat.pos_of_ne_zero fun h => by simp [h] at hx0
no goals
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : ↑(val x) ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
h : val x = 0
⊢ False
simp [h] at hx0
no goals
n : ℕ
hn : Fact (n % 2 = 1)
x : ZMod n
hx0 : x ≠ 0
npos : NeZero n
_hn2 : n / 2 < n
hn2' : n - n / 2 = n / 2 + 1
hxn : n - val x < n
⊢ val x ≤ n / 2 ↔ n / 2 < val (-x)
conv =>
  rhs
  rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← hn2', ← zero_add (-x), ← ZMod.nat_cast_self, ←
    sub_eq_add_neg, ← ZMod.nat_cast_zmod_val x, ← Nat.cast_sub x.val_le, ZMod.val_nat_cast,
    Nat.mod_eq_of_lt hxn, tsub_le_tsub_iff_left x.val_le]