The length of a concatenation is the sum of the lengths

Exercise · length_append'

The length of a concatenation is the sum of the lengths.

Formal statement · Lean 4.lean

theorem length_append' (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length := by
  sorry

Proof. sorry

Nobody has tried yet.