fact: Fixpoint positive_to_int_rec (n:nat) (p:positive) := match n, p with | O, _ => (Npos p, 0) | S n, xH => (0%N, 1) | S n, xO p => let (N,i) := positive_to_int_rec n p in (N, i << 1) | S n, xI p => let (N,i) := positive_to_int_rec n p in (N, (i << 1) + 1) end.
imports: CyclicAxioms ZArith Uint63