proposition: Lemma for_last_char_nil (str : String) P : length str = 0 -> for_last_char str P.
proof: Proof. intros H ch H'. apply length_singleton in H'. rewrite ?take_length, ?drop_length, H in H'. simpl in H'; 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.Common