proposition: Lemma normalP (p : {poly R}) : reflect (normal_spec p) (p \is normal).
proof: Proof. apply/(iffP idP) => [H | [] *]. split. + exact: normal_coef_geq0. - exact: normal_lead_coef_gt0. + exact: normal_squares. - exact: normal_some_coef_gt0. exact: prop_normal. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)