proposition: Lemma coprimep_XsubC2 (a b : R) : b - a != 0 -> coprimep ('X - a%:P) ('X - b%:P).
proof: Proof. by move=> bBa_neq0; rewrite coprimep_XsubC rootE hornerXsubC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)