proposition: Lemma ImMil x : 'Im ('i * x) = 'Re x.
proof: Proof. by rewrite ImM Re_i Im_i mul0r mulr1 add0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)