proposition: Lemma complex_realP x : reflect (exists k, x = k%:C) (x \is Num.real).
proof: Proof. case: x=> [a b] /=; rewrite complex_real. by apply: (iffP eqP) => [->|[c []//]]; exists a. 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)