proposition: Lemma polyXsubC_eqp1 (x : R) : ('X - x%:P %= 1) = false.
proof: Proof. by rewrite -size_poly_eq1 size_XsubC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)