[STATEMENT]
lemma Fract_less_zero_iff: "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < b \<Longrightarrow> (Fract a b < 0) = (a < (0::'a))
[PROOF STEP]
by (auto simp add: Zero_fract_def mult_less_0_iff)