law length_drop_sym

bend-mathlib@0.8.1.0 · string.bend:691

import Base

691# Dropping n characters leaves length - n of them, reversed to rewrite toward the simple side.
692law length_drop_sym:
693  for s: String
694  for n: Nat
695  {Nat.sub(String.length(s), n) == String.length(String.drop(s, n)) : Nat}