[STATEMENT]
lemma ang_vec_opposite_opposite:
  assumes "z1 \<noteq> 0" and "z2 \<noteq> 0"
  shows "\<angle> (-z1) (-z2) = \<angle> z1 z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
have "\<angle> (-z1) (-z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
using ang_vec_opposite1[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) ?z2.0 = \<downharpoonright>\<angle> z1 ?z2.0 - pi\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
using ang_vec_opposite2[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) ?z2.0 = \<downharpoonright>\<angle> z1 ?z2.0 - pi\<downharpoonleft>
\<angle> ?z1.0 (- z2) = \<downharpoonright>\<angle> ?z1.0 z2 + pi\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
using canon_ang_id[of pi, symmetric]
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) ?z2.0 = \<downharpoonright>\<angle> z1 ?z2.0 - pi\<downharpoonleft>
\<angle> ?z1.0 (- z2) = \<downharpoonright>\<angle> ?z1.0 z2 + pi\<downharpoonleft>
- pi < pi \<and> pi \<le> pi \<Longrightarrow> pi = \<downharpoonright>pi\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
have "... = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft> = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>
[PROOF STEP]
by (subst canon_ang_diff[symmetric], simp)
[PROOF STATE]
proof (state)
this:
\<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft> = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
by (metis ang_vec_def canon_ang(1) canon_ang(2) canon_ang_id)
[PROOF STATE]
proof (state)
this:
\<angle> (- z1) (- z2) = \<angle> z1 z2

goal:
No subgoals!
[PROOF STEP]
qed