proposition: Lemma sorted_rconsE (leT : rel A) xs x : transitive leT -> sorted leT (rcons xs x) = all (leT^~ x) xs && sorted leT xs.
proof: Proof. move/rev_trans=>Ht; rewrite -(revK (rcons _ _)) rev_rcons rev_sorted /=. by rewrite path_sortedE // all_rev rev_sorted. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)