proposition: Lemma monicXsubC_normal (a : R) : ('X - a%:P) \is normal = (a <= 0).
proof: Proof. rewrite normalE polyseqXsubC /=. by case Ha: (a <= 0); rewrite oppr_ge0 Ha // ltr01. 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)