proposition: Lemma sum_coef_horner : sum_coef = p.[1].
proof: Proof. rewrite horner_coef. apply eq_bigr => i _. by rewrite expr1n mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist