proposition: Lemma Im_rect : {in real &, forall x y, 'Im (x + 'i * y) = y}.
proof: Proof. move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ImP x Rx) add0r. by rewrite ImMr // Im_i mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)