proposition: Lemma fold'_drop {A} (f : Char -> A -> A) (init : A) (str : String) len m (H' : m + len <= length str) : fold' f init str len = fold' f init (drop m str) len.
proof: Proof. revert str m H'. induction len; simpl. { intros; reflexivity. } { intros. rewrite !(@get_drop (length _ - _)). rewrite drop_length, drop_drop. rewrite <- Nat.sub_add_distr, (Nat.add_comm m), Nat.sub_add_distr, Nat.sub_add by omega. match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end. { rewrite <- IHlen by omega; reflexivity. } { reflexivity. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Le Fiat.Common.Tactics.SetoidSubst Fiat.Common.Tactics.IsClosed Fiat.Parsers.StringLike.Core Fiat.Common.UIP