# Theory Complex_Order

```(*
Title:    HOL/Library/Complex_Order.thy
Author:   Dominique Unruh, University of Tartu

Instantiation of complex numbers as an ordered set.
*)

theory Complex_Order
imports Complex_Main
begin

instantiation complex :: order begin

definition ‹x < y ⟷ Re x < Re y ∧ Im x = Im y›
definition ‹x ≤ y ⟷ Re x ≤ Re y ∧ Im x = Im y›

instance
apply standard
by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff)
end

lemma nonnegative_complex_is_real: ‹(x::complex) ≥ 0 ⟹ x ∈ ℝ›

lemma complex_is_real_iff_compare0: ‹(x::complex) ∈ ℝ ⟷ x ≤ 0 ∨ x ≥ 0›
using complex_is_Real_iff less_eq_complex_def by auto

instance complex :: ordered_comm_ring
apply standard
by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff mult_left_mono mult_right_mono)

instance complex :: ordered_real_vector
apply standard
by (auto simp: less_complex_def less_eq_complex_def mult_left_mono mult_right_mono)

instance complex :: ordered_cancel_comm_semiring
by standard

end
```