[STATEMENT]
lemma min_maxsimpchainD_min_betw:
  "min_maxsimpchain (x#xs@[y]) \<Longrightarrow> maxsimpchain (x#ys@[y]) \<Longrightarrow>
    length ys \<ge> length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>min_maxsimpchain (x # xs @ [y]); maxsimpchain (x # ys @ [y])\<rbrakk> \<Longrightarrow> length xs \<le> length ys
[PROOF STEP]
using is_arg_minD2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_arg_min ?m ?P ?x; ?P ?y\<rbrakk> \<Longrightarrow> \<not> ?m ?y < ?m ?x

goal (1 subgoal):
 1. \<lbrakk>min_maxsimpchain (x # xs @ [y]); maxsimpchain (x # ys @ [y])\<rbrakk> \<Longrightarrow> length xs \<le> length ys
[PROOF STEP]
by fastforce