proposition: Lemma positives_flatten_app xs ys : positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
proof: Proof. unfold positives_flatten. revert ys. induction xs as [|x xs IH]; intros ys; simpl. - rewrite (left_id_L 1 (++)). reflexivity. - rewrite positives_flatten_go_app, (positives_flatten_go_app xs). rewrite IH. rewrite (assoc_L (++)). reflexivity. Qed.
imports: stdpp(options)