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