[STATEMENT]
lemma phl_cons2: "w \<le> x \<Longrightarrow> z \<cdot> y \<le> y \<cdot> w \<Longrightarrow> z \<cdot> y \<le> y \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> x; z \<cdot> y \<le> y \<cdot> w\<rbrakk> \<Longrightarrow> z \<cdot> y \<le> y \<cdot> x
[PROOF STEP]
using local.order_trans mult_isol
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y

goal (1 subgoal):
 1. \<lbrakk>w \<le> x; z \<cdot> y \<le> y \<cdot> w\<rbrakk> \<Longrightarrow> z \<cdot> y \<le> y \<cdot> x
[PROOF STEP]
by blast