fact: Fixpoint digits_aux m nb { struct m } := match m with | xH => nb | xO p => digits_aux p (Pos.succ nb) | xI p => digits_aux p (Pos.succ nb) end.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig