proposition: Lemma sortedPn (s : seq A) : reflect (exists2 x, s = x.2.1 ++ [:: x.1.1, x.1.2 & x.2.2] & (x.1.2 < x.1.1)%O) (~~ sorted <=%O s).
proof: Proof. elim: s => [|a [|b s] IH]. - by apply: (iffP idP) => // [[[x1 [[|x x21] x22]]]]. - by apply: (iffP idP) => // [[[x1 [[|x [| y x21]] x22] []]]]. rewrite /= negb_and; case: leP => [aLb | bLa] /=; last first. by apply: (iffP idP) => // _; exists ((a, b), ([::], s)). apply: (iffP IH) => [] [[[x1 x2] [s1 s2]] /= blE x2Lx1] /=. by exists ((x1, x2), (a :: s1, s2)) => //=; rewrite blE. case: s1 blE => [[aE bE lE]|x3 s1 [aE blE]]. by move: aLb; rewrite aE bE leNgt x2Lx1. by exists ((x1, x2), (s1, s2)). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)