src/HOL/Fields.thy

 lemma divide_less_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
 by (auto simp add: divide_less_eq)
 
 lemma divide_less_eq_1_neg [simp]:
-  "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
+  "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b"
 by (auto simp add: divide_less_eq)
 
 lemma eq_divide_eq_1 [simp]:
   "(1 = b/a) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: eq_divide_eq)