[STATEMENT]
lemma (in Group) lcs_in_Gp:"\<lbrakk>G \<guillemotright> H; G \<guillemotright> K; K \<subseteq> H; a \<in> H\<rbrakk>  \<Longrightarrow> 
                                       a \<diamondsuit> K = a \<diamondsuit>\<^bsub>(Gp G H)\<^esub> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<guillemotright> H ; G \<guillemotright> K ; K \<subseteq> H; a \<in> H\<rbrakk> \<Longrightarrow> a \<diamondsuit> K = a \<diamondsuit>\<^bsub>\<natural>H\<^esub> K
[PROOF STEP]
by (simp add:lcs_def, simp add:Gp_def)