proposition: Lemma last_char_in__app_or_iff (str : String) (ls1 ls2 : list Char) : last_char_in str (ls1 ++ ls2) <-> (last_char_in str ls1 \/ last_char_in str ls2).
proof: Proof. unfold last_char_in. setoid_rewrite List.in_app_iff. generalize (singleton_exists (drop (pred (length str)) str)). rewrite drop_length. case_eq (length str). { intros H _. split; intro H0; [ left; apply last_char_in_empty | apply for_last_char_nil ]; assumption. } { intros ? ? H. simpl in *. specialize_by omega. destruct H as [ch H]. rewrite !(for_last_char__drop n str) by omega. rewrite <- !for_last_char_singleton by eassumption; tauto. } 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