proposition: Lemma nseq_cat_sortedE (s : seq bool) m1 m2 m3 m4 : sorted (<=%O) s -> perm_eq s (nseq m1 false ++ nseq m2 true ++ nseq m3 false ++ nseq m4 true) -> s = nseq (m1 + m3) false ++ nseq (m2 + m4) true.
proof: Proof. move=> /isorted_boolP[[u v] ->] /allP; set s1 := _ ++ _ => permH. congr (nseq _ _ ++ nseq _ _). have [/permH/=|] := boolP (false \in s1). by rewrite !(count_cat, count_nseq) /= !(mul0n, mul1n, addn0, add0n) =>/eqP. by rewrite !(mem_cat, mem_nseq) /= eqxx !negb_or /=; case: (m1) => [|k1]; case: (m3) => [|k2]; rewrite ?(andbF, andbT) //; case: (u). have [/permH/=|] := boolP (true \in s1). by rewrite !(count_cat, count_nseq) /= !(mul0n, mul1n, addn0, add0n) =>/eqP. by rewrite !(mem_cat, mem_nseq) /= eqxx !negb_or /=; case: (m2) => [|k1]; case: (m4) => [|k2]; rewrite ?(andbF, andbT) //; case: (v). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)