proposition: Lemma dsorted_bool_nseq (b : bool) k : (sorted >=%O (nseq k b)).
proof: Proof. case: b; apply/dsorted_boolP; first by exists (k, 0); rewrite cats0. by exists (0, k). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)