proposition: Lemma normal_neq0 (p : {poly R}) : p \is normal -> p != 0.
proof: Proof. move=> /normalP [_ H _ _]; rewrite -lead_coef_eq0. by case: ltrgtP H. 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)