proposition: Lemma compute_next_bin_op'_recr {HSLP : StringLikeProperties Char} (str : String) : compute_next_bin_op' str = match get 0 str with | Some ch => compute_next_bin_op'_step ch (compute_next_bin_op' (drop 1 str)) | None => fun _ => None end.
proof: Proof. apply fold_recr. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.SetoidInstances Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced