proposition: Lemma positives_unflatten_go_app p suffix xs acc : positives_unflatten_go (suffix ++ Pos.reverse (Pos.dup p)) xs acc = positives_unflatten_go suffix xs (acc ++ p).
proof: Proof. revert suffix acc. induction p as [p IH|p IH|]; intros acc suffix; simpl. - rewrite 2!Pos.reverse_xI. rewrite 2!(assoc_L (++)). rewrite IH. reflexivity. - rewrite 2!Pos.reverse_xO. rewrite 2!(assoc_L (++)). rewrite IH. reflexivity. - reflexivity. Qed.
imports: stdpp(options)