law length_drop

bend-mathlib@0.8.1.0 · string.bend:462

import Base

462# Dropping n characters leaves length - n of them.
463law length_drop:
464  for s: String
465  for n: Nat
466  {String.length(String.drop(s, n)) == Nat.sub(String.length(s), n) : Nat}