proposition: Lemma after_last_char_such_that_after_end {str : String} {P} {n} (Hle : length str <= n) : is_after_last_char_such_that str n P <-> for_last_char str P .
proof: Proof. unfold is_after_last_char_such_that. rewrite take_long by omega. split; intro; destruct_head_hnf and; destruct_head_hnf or; destruct_head_hnf and; repeat split; trivial; try rewrite Nat.min_idempotent in *; try solve [ left; assumption | right; omega | apply for_last_char_nil; omega | apply forall_chars_nil; rewrite ?drop_length, ?take_length; try apply Nat.min_case_strong; intros; omega | destruct (length str); try solve [ left; repeat split; eauto; omega | right; repeat split; eauto; 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