proposition: Lemma isorted_noFT s : (sorted <=%O s) = (s == nseq (noF s) false ++ nseq (noT s) true).
proof: Proof. apply/isorted_boolP/eqP => [[[i j]->]|->]; first by rewrite !noE. by exists (noF s, noT s). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)