proposition: Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) : length xs = length ys → p1 ++ positives_flatten xs = p2 ++ positives_flatten ys → xs = ys.
proof: Proof. revert p1 p2 ys; induction xs as [|x xs IH]; intros p1 p2 [|y ys] ?; simplify_eq/=; auto. rewrite !positives_flatten_cons, !(assoc _); intros Hl. assert (xs = ys) as <- by eauto; clear IH; f_equal. apply (inj (.++ positives_flatten xs)) in Hl. rewrite 2!Pos.reverse_dup in Hl. apply (Pos.dup_suffix_eq _ _ p1 p2) in Hl. by apply (inj Pos.reverse). Qed.
imports: stdpp(options)