fact: Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive := match xs with | [] => acc | x :: xs => positives_flatten_go xs (acc~1~0 ++ Pos.reverse (Pos.dup x)) end.
imports: stdpp(options)