fact: Fixpoint constant_getter_aux n cst := match n, cst with | O, Consts (HConst xi) _ => xi | S p, Consts _ c => constant_getter_aux p c end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float