proposition: Lemma for_last_char_False (str : String) P : (forall ch, ~P ch) -> for_last_char str P -> length str = 0.
proof: Proof. intros H' H. case_eq (length str); trivial. pose proof (singleton_exists (drop (pred (length str)) str)) as H''. rewrite drop_length in H''. intros n H'''. rewrite H''' in *. simpl in *. specialize_by omega. destruct H'' as [ch H'']. apply (for_last_char__drop n) in H; [ | omega ]. apply (for_last_char_singleton _ _ _ H'') in H. specialize (H' ch). exfalso; eauto. 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