proposition: Lemma ImM x y : 'Im (x * y) = 'Re x * 'Im y + 'Re y * 'Im x.
proof: Proof. rewrite [x in LHS]Crect [y in LHS]Crect mulC_rect. by rewrite !(Im_rect, rpredB, rpredD, rpredM). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)