fact: Definition smaller_sizes (sz : size) : list size := match sz with | Sanity => [] | SuperFast => [Sanity] | Fast => [Sanity; SuperFast] | Medium => [Sanity; SuperFast; Fast] | Slow => [Sanity; SuperFast; Fast; Medium] | VerySlow => [Sanity; SuperFast; Fast; Medium; Slow] end.
imports: Coq.QArith.QArith Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.Lists.List Coq.ZArith.ZArith PerformanceExperiments.Sandbox