proposition: Lemma eqC x y : (x == y) = ('Re x == 'Re y) && ('Im x == 'Im y).
proof: Proof. by apply/eqP/(andPP eqP eqP) => /eqCP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)