proposition: Lemma coprimep_factor (a b : R) : (b - a)%R \is a GRing.unit -> coprimep ('X - a%:P) ('X - b%:P).
proof: Proof. move=> Hab; apply/Bezout_coprimepP. exists ((b - a)^-1%:P, -(b - a) ^-1%:P). rewrite /= !mulrBr !mulNr opprK -!addrA (addrC (- _)) !addrA addrN. by rewrite add0r -mulrBr -rmorphB -rmorphM mulVr // eqpxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)