proposition: Lemma Im_conj z : 'Im z^* = - 'Im z.
proof: Proof. by rewrite !ImE -mulNr -mulrN opprB conjCK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)