NeZero cons

Stream: lean4

[Wrenna Robson]

I'm adding this to Batteries in a current PR (I need it for some examples), but honestly I think this would be great in core (and possibly equivalents for Array and Vector?)

instance instNeZeroNatLengthCons {a : α} {l : List α} : NeZero (a :: l).length :=
  ⟨Nat.succ_ne_zero _⟩

In particular what this allows you to do is use numerals for things like Fin ["a", "b", "c"].length without getting an error, which is rather useful.