fact: Fixpoint positive_aux_to_num (p : positive) (i j : int) : number := match p with | xH => (i + j) :: nil | xO p1 => let i1 := 2 * i in match i1 ?= 0 with | Gt => positive_aux_to_num p1 i1 j | _ => j :: positive_aux_to_num p1 1 0 end | xI p1 => let i1 := 2 * i in let j1 := i + j in match i1 ?= 0 with | Gt => positive_aux_to_num p1 i1 j1 | _ => j1 :: positive_aux_to_num p1 1 0 end end.
imports: List ZArith Znumtheory Uint63 Cyclic63