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