proposition: Lemma irredp_XsubC (x : R) : irreducible_poly ('X - x%:P).
proof: Proof. split=> [|d size_d d_dv_Xx]; first by rewrite size_XsubC. have: ~ d %= 1 by apply/negP; rewrite -size_poly_eq1. have [|m /=] := @dvdp_prod_XsubC _ [:: x] id d; first by rewrite big_seq1. by case: m => [|[] [|_ _] /=]; rewrite (big_nil, big_seq1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)