k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * pred (q + 1) = 0 + ↑k * (q + 1)
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑(modDivAux k 0 (q + 1)).fst + ↑k * (modDivAux k 0 (q + 1)).snd = 0 + ↑k * (q + 1)
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)
no goals
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * pred (q + 1) = 0 + ↑k * (q + 1)
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]