proposition: Lemma positives_flatten_suffix (l k : list positive) : l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
proof: Proof. intros [l' ->]. exists (positives_flatten l'). apply positives_flatten_app. Qed.
imports: stdpp(options)