proposition: Lemma monicXsubCe (c:R) i : ('X - c%:P) ^+ i \is monic.
proof: Proof. apply:monic_exp; exact: monicXsubC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)