proposition: Lemma positives_unflatten_flatten_go suffix xs acc : positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 = positives_unflatten_go suffix (xs ++ acc) 1.
proof: Proof. revert suffix acc. induction xs as [|x xs IH]; intros suffix acc; simpl. - reflexivity. - rewrite positives_flatten_go_app. rewrite (assoc_L (++)). rewrite IH. rewrite (assoc_L (++)). rewrite positives_unflatten_go_app. simpl. rewrite (left_id_L 1 (++)). reflexivity. Qed.
imports: stdpp(options)