fact: Fixpoint find_just_below_max_size {T} (avg : T -> T -> T) (size : T -> Q) (max_size : Q) (t_lo t_hi : T) (fuel : nat) : T := match fuel with | O => t_lo | S fuel => let sz_lo := size t_lo in let sz_hi := size t_hi in if Qeq_bool sz_lo sz_hi then t_lo else let t_mid := avg t_lo t_hi in let sz_mid := size t_mid in if (Qeq_bool sz_lo sz_mid || Qeq_bool sz_mid sz_hi) then t_lo else let '(t_lo, t_hi) := if Qle_bool max_size sz_mid then (t_lo, t_mid) else (t_mid, t_hi) in find_just_below_max_size avg size max_size t_lo t_hi fuel 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