fact: Fixpoint root_plain_aux depth prec prog bounds xi loc := match depth with | S depth => let xi' := A.DiffValuator.root prec prog bounds xi in if I.is_empty xi' then xi' else if fast_enough prec xi xi' then root_plain_aux depth prec prog bounds xi' loc else let (xi1,xi2) := I.bisect xi' in match loc with | Eq => let xi1' := root_plain_aux depth prec prog bounds xi1 Lt in if I.is_empty xi1' then root_plain_aux depth prec prog bounds xi2 Eq else let xi2' := root_plain_aux depth prec prog bounds xi2 Gt in if I.is_empty xi2' then I.join xi1' (root_plain_aux depth prec prog bounds xi1 Gt) else I.join xi1' xi2' | Lt => let xi1' := root_plain_aux depth prec prog bounds xi1 Lt in if I.is_empty xi1' then root_plain_aux depth prec prog bounds xi2 Lt else xi1' | Gt => let xi2' := root_plain_aux depth prec prog bounds xi2 Gt in if I.is_empty xi2' then root_plain_aux depth prec prog bounds xi1 Gt else xi2' end | O => xi end.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify Interval_helper