proposition: Lemma substring_min {x x' y y' z str} (H : substring x y str =s substring x' y' str) : substring x (min y z) str =s substring x' (min y' z) str.
proof: Proof. pose proof (fun y x => @substring_substring str 0 z x y) as H'; simpl in *. setoid_rewrite Nat.sub_0_r in H'. setoid_rewrite Nat.min_comm in H'. rewrite <- !H', H; 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