n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val (-a) = if a = 0 then 0 else n - val a
rw [neg_val']
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - val a) % n = if a = 0 then 0 else n - val a

case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
by_cases h : a = 0
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - val a) % n = n - val a
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
rw [if_neg h]
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - val a < n
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - val a) % n = n - val a
apply Nat.mod_eq_of_lt
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ 0 < val a
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - val a < n
apply Nat.sub_lt (NeZero.pos n)
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val a ≤ 0
⊢ a = 0
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ 0 < val a
contrapose! h
no goals
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val a ≤ 0
⊢ a = 0
rwa [le_zero_iff, val_eq_zero] at h
no goals
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]