proposition: Lemma for_last_char_True (str : String) (P : _ -> Prop) (p : forall ch, P ch) : for_last_char str P.
proof: Proof. destruct (length str) eqn:H. { apply for_last_char_nil; assumption. } { rewrite for_last_char_exists by omega. destruct (get 0 (drop (pred (length str)) str)) as [ch|] eqn:Heq. { exists ch; split; auto. rewrite is_char_parts. rewrite drop_length; split; [ omega | assumption ]. } { apply no_first_char_empty in Heq. rewrite drop_length, H in Heq. simpl in *; 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