fact: Fixpoint positives_unflatten_go (p : positive) (acc_xs : list positive) (acc_elm : positive) : option (list positive) := match p with | 1 => Some acc_xs | p'~0~0 => positives_unflatten_go p' acc_xs (acc_elm~0) | p'~1~1 => positives_unflatten_go p' acc_xs (acc_elm~1) | p'~1~0 => positives_unflatten_go p' (acc_elm :: acc_xs) 1 | _ => None end%positive.
imports: stdpp(options)