proposition: Lemma for_last_char_exists_get (str : String) P (H : length str >= 1) : for_last_char str P <-> (exists ch, get (pred (length str)) str = Some ch /\ P ch).
proof: Proof. rewrite for_last_char_exists by assumption. split; intros [ch [H0 H1]]; exists ch; (split; [ | assumption ]); revert H0; rewrite get_drop, <- get_0; rewrite take_long by (rewrite drop_length; omega); trivial. 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