feat: change List.length_cons to use + 1 instead of succ (#4500)

The simp normal form of `succ` is `+ 1`, this changes `List.length_cons`
to use that normal form.

src/Init/Data/List/Basic.lean

@@ -67,6 +67,9 @@ namespace List
 
 @[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl
 
+@[simp] theorem length_cons {α} (a : α) (as : List α) : (cons a as).length = as.length + 1 :=
+  rfl
+
 /-! ### set -/
 
 @[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by

src/Init/Prelude.lean

@@ -2329,9 +2329,6 @@ without running out of stack space.
 def List.lengthTR (as : List α) : Nat :=
   lengthTRAux as 0
 
-@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
-  rfl
-
 /--
 `as.get i` returns the `i`'th element of the list `as`.
 This version of the function uses `i : Fin as.length` to ensure that it will