proposition: Lemma substring_substring {s n m n' m'} : substring n m (substring n' m' s) = substring (n + n') (min m (m' - n)) s.
proof: Proof. revert n m n' m'. induction s; intros. { destruct n, m, n', m'; reflexivity. } { destruct n', m'; rewrite <- ?Nat.add_0_r, <- ?Nat.sub_0_r, ?Nat.min_0_r, ?Nat.min_0_l; destruct n, m; trivial; simpl; rewrite ?IHs, ?substring_correct0, <- ?plus_n_O, ?Nat.sub_0_r; simpl; try reflexivity. rewrite (Nat.add_comm _ (S _)); simpl. rewrite (Nat.add_comm n n'). reflexivity. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Fiat.Common.List.Operations Fiat.Common.StringOperations