fact: Fixpoint substring (n m : nat) (s : string) : string := match n, m, s with | O, O, _ => EmptyString | O, S m', EmptyString => s | O, S m', String c s' => String c (substring 0 m' s') | S n', _, EmptyString => s | S n', _, String c s' => substring n' m s' end.
imports: Arith Ascii Bool Coq.Strings.Byte