fact: Definition compose_poly (f : polynomial) (x : polynomial) : polynomial := eval_poly_gen poly_add (fun p e => poly_power p (Z.to_N e) ) (fun c p => poly_mul [(c, 0%Z)] p ) [] f x.
imports: Coq.Strings.String Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax Coq.NArith.NArith Coq.ZArith.ZArith Coq.Arith.Arith Coq.Lists.List PerformanceExperiments.LetIn