fact: Fixpoint subdivide {T} {HDA : has_double_avg T} (min : T) (max : T) (lg2_n_parts : nat) : list (T * T) := match lg2_n_parts with | O => [(min, max)] | S lg2_n_parts => let mid := avg_T min max in subdivide min mid lg2_n_parts ++ subdivide mid max lg2_n_parts end.
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