fact: Definition map_double (ls : list Z) := list_rect _ nil (fun x xs rec => dlet y := x + x in y :: rec) ls.
imports: Coq.micromega.Lia Coq.ZArith.ZArith Coq.QArith.QArith Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Lists.List PerformanceExperiments.Harness PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances