proposition: Lemma sorted_cat_cons_cat (l r : seq A) x : sorted ord (l ++ x :: r) = sorted ord (l ++ [::x]) && sorted ord (x::r).
proof: Proof. rewrite !(sorted_pairwise (@trans A)) cats1 pairwise_cat pairwise_rcons allrel_consr !pairwise_cons. case/boolP: (all (ord^~ x) l)=>//= Hl; case/boolP: (all (ord x) r)=>/= [Hr|_]; last by rewrite !andbF. by rewrite (allrel_trans (@trans A) Hl Hr). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)