n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (digits b' n) [MOD b]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ List.sum (digits b' n) [MOD b]
rw [← ofDigits_one]
case h.e'_3.h.e'_3
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (digits b' n) ≡ ofDigits 1 (digits b' n) [MOD b]
convert ofDigits_modEq b' b (digits b' n)
no goals
case h.e'_3.h.e'_3
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b
exact h.symm