proposition: Lemma map_polyXsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) x : map_poly f ('X - x%:P) = 'X - (f x)%:P.
proof: Proof. by rewrite rmorphB/= map_polyX map_polyC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)