proposition: Lemma irredp_XsubCP d p : irreducible_poly p -> d %| p -> {d %= 1} + {d %= p}.
proof: Proof. move=> irred_p dvd_dp; have [] := boolP (_ %= 1); first by left. by rewrite -size_poly_eq1=> /irred_p /(_ dvd_dp); right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)