proposition: Lemma find_first_char_such_that'_S {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} (P : Char -> bool) (len : nat) (str : String) : find_first_char_such_that' P (S len) str = let otherwise := S (find_first_char_such_that' P len str) in match get (length str - S len) str with | Some ch => if P ch then 0 else otherwise | None => otherwise end.
proof: Proof. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.PeanoNat Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.StringLike.FirstChar Fiat.Common Fiat.Common.NatFacts