proposition: Lemma positives_flatten_cons x xs : positives_flatten (x :: xs) = 1~1~0 ++ Pos.reverse (Pos.dup x) ++ positives_flatten xs.
proof: Proof. change (x :: xs) with ([x] ++ xs)%list. rewrite positives_flatten_app. rewrite (assoc_L (++)). reflexivity. Qed.
imports: stdpp(options)