proposition: Lemma ndot_ne_disjoint N x y : x ≠ y → N.@x ## N.@y.
proof: Proof. intros Hxy a. unfold up_close. rewrite !nclose_unseal, !ndot_unseal. unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes. intros [qx ->] [qy Hqy]. revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq. Qed.
imports: stdpp(options)