fact: Definition hornerE_comm := (hornerD, hornerN, hornerX, hornerC, horner_cons, simp, hornerCM, hornerZ, (fun p x => hornerM_comm p (comm_polyX x))).
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)