[STATEMENT]
lemma pgallery_least_length:
  assumes "chamber C" "chamber D" "C\<noteq>D"
  defines "Cs \<equiv> ARG_MIN length Cs. gallery (C#Cs@[D])"
  shows   "pgallery (C#Cs@[D])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgallery (C # Cs @ [D])
[PROOF STEP]
using   assms min_gallery_least_length min_gallery_pgallery
[PROOF STATE]
proof (prove)
using this:
chamber C
chamber D
C \<noteq> D
Cs \<equiv> ARG_MIN length Cs. gallery (C # Cs @ [D])
\<lbrakk>chamber ?C; chamber ?D; ?C \<noteq> ?D\<rbrakk> \<Longrightarrow> min_gallery (?C # (ARG_MIN length Cs. gallery (?C # Cs @ [?D])) @ [?D])
min_gallery ?xs \<Longrightarrow> pgallery ?xs

goal (1 subgoal):
 1. pgallery (C # Cs @ [D])
[PROOF STEP]
by      fast