src/HOL/Library/Extended.thy

 "(_::'a extended) \<le> _     = False"
 
 case_of_simps less_eq_extended_case: less_eq_extended.simps
 
 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
-"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
+"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
 
 instance
   by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
 
 end