fact: Definition iter_plus_acc (m : nat) (acc v : Z) := @nat_rect (fun _ => Z -> Z) (fun acc => acc) (fun _ rec acc => rec (acc + v)) m acc.
imports: Coq.micromega.Lia Coq.ZArith.ZArith Coq.QArith.QArith Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Lists.List PerformanceExperiments.Harness