proposition: Lemma complex_real (a b : R) : a +i* b \is Num.real = (b == 0).
proof: Proof. rewrite realE; simpc; rewrite [0 == _]eq_sym. by have [] := ltrgtP 0 a; rewrite ?(andbF, andbT, orbF, orbb). 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)