fact: Fixpoint nat_of_pos_rec_expand (p : positive) (a : nat) : nat := match p with | p0~1 => addn_expand a (nat_of_pos_rec_expand p0 (addn_expand a a)) | p0~0 => nat_of_pos_rec_expand p0 (addn_expand a a) | 1 => a end%positive.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)