proposition: Lemma substring_take_drop (str : String) n m : String.substring n m str = take m (drop n str).
proof: Proof. simpl. rewrite substring_substring; simpl. apply Nat.min_case_strong; simpl; trivial; []. intro H. apply substring_correct4; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.Ascii Coq.Strings.String Coq.ZArith.ZArith Coq.Arith.PeanoNat Fiat.Common Fiat.Common.Equality Fiat.Common.StringOperations Fiat.Common.StringFacts Fiat.Parsers.StringLike.Core