[STATEMENT]
lemma pos_oriented_opposite_ocircline_cmat [simp]:
  assumes "hermitean H \<and> H \<noteq> mat_zero"
  shows  "pos_oriented_cmat (opposite_ocircline_cmat H) \<longleftrightarrow> \<not> pos_oriented_cmat H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
obtain A B C D where HH: "H = (A, B, C, D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. H = (A, B, C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases H) auto
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
hence "Re A = 0 \<and> Re D = 0 \<longrightarrow> B \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)

goal (1 subgoal):
 1. is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
[PROOF STEP]
using assms hermitean_elems[of A B C D]
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)
hermitean H \<and> H \<noteq> mat_zero
hermitean (A, B, C, D) \<Longrightarrow> is_real A
hermitean (A, B, C, D) \<Longrightarrow> is_real D
hermitean (A, B, C, D) \<Longrightarrow> B = cnj C
hermitean (A, B, C, D) \<Longrightarrow> cnj B = C

goal (1 subgoal):
 1. is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
[PROOF STEP]
by (cases A, cases D) (auto simp add: Complex_eq)
[PROOF STATE]
proof (state)
this:
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
have "B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
[PROOF STEP]
using canon_ang_plus_pi2[of "Arg B"] Arg_bounded[of B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>- 2 * pi < Arg B; Arg B \<le> 0\<rbrakk> \<Longrightarrow> \<downharpoonright>Arg B + pi\<downharpoonleft> = Arg B + pi
- pi < Arg B \<and> Arg B \<le> pi

goal (1 subgoal):
 1. B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
[PROOF STEP]
by (auto simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
have "B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)
[PROOF STEP]
using canon_ang_plus_pi1[of "Arg B"] Arg_bounded[of B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < Arg B; Arg B \<le> 2 * pi\<rbrakk> \<Longrightarrow> \<downharpoonright>Arg B + pi\<downharpoonleft> = Arg B - pi
- pi < Arg B \<and> Arg B \<le> pi

goal (1 subgoal):
 1. B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)
[PROOF STEP]
by (auto simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H = (A, B, C, D)
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)
[PROOF STEP]
show "pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)"
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
by simp (metis not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)

goal:
No subgoals!
[PROOF STEP]
qed