[STATEMENT]
lemma ennreal_mult_le_mult_iff: "c \<noteq> 0 \<Longrightarrow> c \<noteq> top \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> (b :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<noteq> 0; c \<noteq> top\<rbrakk> \<Longrightarrow> (c * a \<le> c * b) = (a \<le> b)
[PROOF STEP]
including ennreal.lifting
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<noteq> 0; c \<noteq> top\<rbrakk> \<Longrightarrow> (c * a \<le> c * b) = (a \<le> b)
[PROOF STEP]
by (transfer, subst ereal_mult_le_mult_iff) (auto simp: top_ereal_def)