English
For lists l1 and l2 of equal length, the sum of the numbers represented by ofDigits b l1 and ofDigits b l2 equals the number represented by ofDigits b applied to the pointwise sum (zipWith (+) l1 l2).
Русский
Для списков равной длины сумма чисел, представляемых by ofDigits b l1 и by ofDigits b l2, равна числу, представленному ofDigits b (zipWith (+) l1 l2).
LaTeX
$$$ \\text{l1,l2 : List Nat},\\ \\mathrm{length}(l1)=\\mathrm{length}(l2)\\Rightarrow \\mathrm{ofDigits}(b,l1) + \\mathrm{ofDigits}(b,l2) = \\mathrm{ofDigits}(b,\\mathrm{zipWith}(+)\\, l1\, l2) $$$
Lean4
/-- The addition of ofDigits of two lists is equal to ofDigits of digit-wise addition of them -/
theorem ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : ℕ} {l1 l2 : List ℕ} (h : l1.length = l2.length) :
ofDigits b l1 + ofDigits b l2 = ofDigits b (l1.zipWith (· + ·) l2) := by
induction l1 generalizing l2 with
| nil => simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]
| cons hd₁ tl₁ ih₁ =>
induction l2 generalizing tl₁ with
| nil => simp_all
| cons hd₂ tl₂
ih₂ =>
simp_all only [List.length_cons, ofDigits_cons, add_left_inj, eq_comm, List.zipWith_cons_cons]
rw [← ih₁ h.symm, mul_add]
ac_rfl
