[STATEMENT]
lemma circ_decompose_12:
  "x\<^sup>\<circ> * y\<^sup>\<circ> \<le> (x\<^sup>\<circ> * y)\<^sup>\<circ> * x\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<circ> * y\<^sup>\<circ> \<le> (x\<^sup>\<circ> * y)\<^sup>\<circ> * x\<^sup>\<circ>
[PROOF STEP]
by (metis circ_sup_9 circ_sub_dist_3)