[STATEMENT]
lemma in_ocircline_ounit_circle_conjugate [simp]:
  assumes "in_ocircline ounit_circle z"
  shows "in_ocircline ounit_circle (conjugate z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_ocircline ounit_circle (conjugate z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
in_ocircline ounit_circle z

goal (1 subgoal):
 1. in_ocircline ounit_circle (conjugate z)
[PROOF STEP]
by (transfer, transfer, auto simp add: vec_cnj_def)