chore: add helper theorems

src/Init/Data/Nat/Basic.lean

@@ -296,6 +296,14 @@ theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
     have : a < b := Nat.lt_trans (Nat.lt_succ_self _) h
     zero_lt_of_lt this
 
+theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a := by
+  match a with
+  | 0 => contradiction
+  | a+1 => apply Nat.zero_lt_succ
+
+theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b :=
+  fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
+
 theorem le_or_eq_or_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n :=
   Decidable.byCases
     (fun (h' : m = succ n) => Or.inr h')

src/Init/Data/String/Extra.lean

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 prelude
 import Init.Control.Except
 import Init.Data.ByteArray
+import Init.SimpLemmas
+import Init.Data.Nat.Linear
 import Init.Util
 
 namespace String
@@ -25,4 +27,16 @@ constant fromUTF8Unchecked (a : @& ByteArray) : String
 @[extern "lean_string_to_utf8"]
 constant toUTF8 (a : @& String) : ByteArray
 
+theorem one_le_csize (c : Char) : 1 ≤ csize c := by
+  simp [csize, Char.utf8Size]
+  repeat (first | split | decide)
+
+theorem eq_empty_of_bsize_eq_zero (h : s.bsize = 0) : s = "" := by
+  match s with
+  | ⟨[]⟩   => rfl
+  | ⟨c::cs⟩ =>
+    simp [bsize, utf8ByteSize, utf8ByteSize.go] at h
+    have : utf8ByteSize.go cs + 1 ≤ utf8ByteSize.go cs + csize c := Nat.add_le_add_left (one_le_csize c) _
+    simp_arith [h] at this
+
 end String