fact: Fixpoint of_pos_rec (n:nat) (p:positive) {struct p} := match n, p with | O, _ => 0 | S n, xH => 1 | S n, xO p => (of_pos_rec n p) << 1 | S n, xI p => (of_pos_rec n p) << 1 lor 1 end.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63