proposition: Lemma horner_mod (R : fieldType) (p q : {poly R}) x : root q x -> (p %% q).[x] = p.[x].
proof: Proof. by move=> /eqP qx0; rewrite [p in RHS](divp_eq p q) !hornerE qx0 mulr0 add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)