proposition: Lemma nclose_subseteq N x : ↑N.@x ⊆ (↑N : coPset).
proof: Proof. intros p. unfold up_close. rewrite !nclose_unseal, !ndot_unseal. unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes. intros [q ->]. destruct (positives_flatten_suffix N (ndot_def N x)) as [q' ?]. { by exists [encode x]. } by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal. Qed.
imports: stdpp(options)