proposition: Lemma positives_unflatten_flatten xs : positives_unflatten (positives_flatten xs) = Some xs.
proof: Proof. unfold positives_flatten, positives_unflatten. replace (positives_flatten_go xs 1) with (1 ++ positives_flatten_go xs 1) by apply (left_id_L 1 (++)). rewrite positives_unflatten_flatten_go. simpl. rewrite (right_id_L [] (++)%list). reflexivity. Qed.
imports: stdpp(options)