[GOAL]
m : ℕ
⊢ ↑(toPNat' (m + 1)) = if 0 < m + 1 then m + 1 else 1
[PROOFSTEP]
rw [if_pos (succ_pos m)]
[GOAL]
m : ℕ
⊢ ↑(toPNat' (m + 1)) = m + 1
[PROOFSTEP]
rfl
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
[PROOFSTEP]
dsimp [mod, modDiv]
[GOAL]
m k : ℕ+
⊢ ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
m k : ℕ+
x✝ : ℕ
⊢ ↑(modDivAux k x✝ (↑m / ↑k)).fst = if x✝ = 0 then ↑k else x✝
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = if zero = 0 then ↑k else zero
[PROOFSTEP]

| zero =>
  rw [if_pos rfl]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = if zero = 0 then ↑k else zero
[PROOFSTEP]
rw [if_pos rfl]
[GOAL]
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = ↑k
[PROOFSTEP]
rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = if succ n = 0 then ↑k else succ n
[PROOFSTEP]

| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = if succ n = 0 then ↑k else succ n
[PROOFSTEP]
rw [if_neg n.succ_ne_zero]
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = succ n
[PROOFSTEP]
rfl
[GOAL]
m k : ℕ+
⊢ div m k = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
dsimp [div, modDiv]
[GOAL]
m k : ℕ+
⊢ (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
m k : ℕ+
x✝ : ℕ
⊢ (modDivAux k x✝ (↑m / ↑k)).snd = if x✝ = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = if zero = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]

| zero =>
  rw [if_pos rfl]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = if zero = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
rw [if_pos rfl]
[GOAL]
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = pred (↑m / ↑k)
[PROOFSTEP]
rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = if succ n = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]

| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = if succ n = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
rw [if_neg n.succ_ne_zero]
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = ↑m / ↑k
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
hn : 0 < n
⊢ ↑↑(Nat.toPNat' (natAbs n)) = n
[PROOFSTEP]
rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'), Int.natAbs_of_nonneg hn.le]
