Theorem: ASCII.String.length_extract (ASCII/Lemmas.lean)

State before:
s : ASCII.String
start stop : Nat
⊢ (s.extract start stop).length = min stop s.length - start
Tactic:
simp [length, ByteArray.size_extract]
State after:
no goals