law take_append_drop_sym

bend-mathlib@0.8.1.0 · string.bend:673

import Base

673# Taking n characters and appending the rest after dropping n gives the string back, reversed to rewrite toward the simple side.
674law take_append_drop_sym:
675  for s: String
676  for n: Nat
677  {s == String.append(String.take(s, n), String.drop(s, n)) : String}