proposition: Lemma positives_flatten_go_app xs acc : positives_flatten_go xs acc = acc ++ positives_flatten_go xs 1.
proof: Proof. revert acc. induction xs as [|x xs IH]; intros acc; simpl. - reflexivity. - rewrite IH. rewrite (IH (6 ++ _)). rewrite 2!(assoc_L (++)). reflexivity. Qed.
imports: stdpp(options)