fact: Fixpoint choose_go {i} (acc : Acc choose_step i) : A := match Some_dec (decode i) with | inleft (x↾Hx) => match decide (P x) with | left _ => x | right H => choose_go (Acc_inv acc (choose_step_Some Hx H)) end | inright H => choose_go (Acc_inv acc (choose_step_None H)) end.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)