fact: Fixpoint find_above_max_size {T} (double : T -> T) (size : T -> Q) (max_size : Q) (ndoublings : nat) (t_prev t_cur : T) (fuel : nat) : T * T * nat := match fuel with | O => (t_prev, t_cur, ndoublings) | S fuel => if Qle_bool max_size (size t_cur) then (t_prev, t_cur, ndoublings) else find_above_max_size double size max_size (S ndoublings) t_cur (double t_cur) 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