proposition: Lemma dsorted_boolP (s : seq bool) : reflect (exists t, let: (j,k) := t in s = nseq j true ++ nseq k false) (sorted >=%O s).
proof: Proof. elim: s => [|[] s IH]. - by apply: (iffP idP) => // _; exists (0,0). - rewrite dsorted_consT; apply: (iffP IH) => [] [[j k]]. by move=> ->; exists (j.+1, k). case: j => /= [|j [->]]; first by case: k. by exists (j, k). rewrite dsorted_consF; apply: (iffP eqP) => [->|[[[|j] k]]] /=. - by exists (0, (size s).+1). - by case: k => [|k /= [->]]; rewrite ?size_nseq. by case. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)