proposition: Lemma is_after_last_char_such_that_eq_nat_iff (str : String) (n n' : nat) P (H0 : is_after_last_char_such_that str n P) (H1 : is_after_last_char_such_that str n' P) : n = n' \/ (n >= length str /\ n' >= length str).
proof: Proof. revert dependent n'; revert dependent str; induction n; intros; [ destruct n'; intros; [ left; reflexivity | ] | destruct n'; intros; [ right; intros | ] ]; [ unfold is_after_last_char_such_that in *; repeat match goal with | _ => assumption | [ H : and _ _ |- _ ] => destruct H | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H') | [ H : _ |- _ ] => rewrite drop_0 in H | [ H : forall_chars _ _, H' : for_last_char _ _ |- ?T ] => apply (forall_chars_for_last_char_overlap (R := T) H H'); solve [ omega | tauto | exfalso; tauto ] | [ H : ?x = 0 |- context[?x] ] => rewrite H | _ => omega | _ => progress destruct_head and | [ H : context[_ - 0] |- _ ] => rewrite Nat.sub_0_r in H | _ => progress destruct_head or | [ |- _ /\ _ ] => split | [ |- 0 = S _ \/ _ ] => right | [ H : for_last_char (take 0 _) _ |- _ ] => clear H | [ H : forall_chars ?str ?P, H' : forall_chars (drop _ ?str) ?P |- _ ] => clear H' | [ H : forall_chars ?str ?P, H' : forall_chars (take _ ?str) ?P |- _ ] => clear H' | _ => right; repeat split; solve [ assumption | omega ] | [ H : forall_chars ?str ?P, H' : for_last_char (take (S ?n) ?str) ?P' |- ?R ] => rewrite forall_chars_take in H; specialize (H n); apply forall_chars__impl__for_last_char in H | [ H : for_last_char ?s ?P, H' : for_last_char ?s ?P' |- ?T' ] => destruct (fun pf => for_last_char_combine (T := T') pf H H'); [ cbv beta; tauto | | ]; clear H H' | [ H : length (take _ _) = 0 |- _ ] => rewrite take_length in H | [ H : min ?x ?y = 0 |- _ ] => revert H; apply (Nat.min_case_strong x y) | _ => intro end.. | let H := fresh in edestruct IHn as [H|H]; [ solve [ eauto using is_after_last_char_such_that_drop ].. | left; omega | right; rewrite drop_length in H; destruct_head and; 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