law is_empty_iff_length_eq_zero_sym

bend-mathlib@0.8.1.0 · string.bend:648

import Base

648# A string is empty exactly when its length is zero, reversed to rewrite toward the simple side.
649law is_empty_iff_length_eq_zero_sym:
650  for s: String
651  {Nat.is_eq(String.length(s), 0n) == String.is_empty(s) : Bool}