proposition: Lemma eq_complex : forall (R : eqType) (x y : complex R), (x == y) = (Re x == Re y) && (Im x == Im y).
proof: Proof. move=> R [a b] [c d] /=. apply/eqP/andP; first by move=> [-> ->]; split. by case; move/eqP->; move/eqP->. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)