fact: Definition integrate_poly (p : polynomial) : polynomial * Q := (List.flat_map (fun '(coeff, exp) => if negb (exp =? -1)%Z then [(coeff / (exp + 1)%Z, (exp + 1)%Z)] else []) p, List.fold_right (fun x y => x + y)%Q 0%Q (List.map (fun '(coeff, exp) => if (exp =? -1)%Z then coeff else 0%Q) p)).
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