proposition: Lemma sorted1 (r : rel A) xs : size xs == 1 -> sorted r xs.
proof: Proof. by case: xs=>// x; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)