proposition: Lemma after_last_char_such_that_nil (str : String) (n : nat) P (Hlen : length str = 0) : is_after_last_char_such_that str n P.
proof: Proof. unfold is_after_last_char_such_that. split; [ apply forall_chars_nil | apply for_last_char_nil ]; rewrite ?take_length, ?drop_length; try apply Nat.min_case_strong; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.StringLike.LastChar Fiat.Common