proposition: Lemma Creal_ImP z : reflect ('Im z = 0) (z \is real).
proof: Proof. rewrite ImE CrealE -subr_eq0 -(can_eq (mulKf neq0Ci)) mulr0. by rewrite -(can_eq (divfK nz2)) mul0r; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)