fact: Fixpoint count_digits_aux nb pow (p q : positive) { struct q } : positive := if Zlt_bool (Zpos p) pow then nb else match q with | xH => nb | xI r => count_digits_aux (Pos.succ nb) (Zmult beta pow) p r | xO r => count_digits_aux (Pos.succ nb) (Zmult beta pow) p r end.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal