proposition: Lemma sorted_oleq s : sorted (@ord T) s -> sorted (@oleq T) s.
proof: Proof. by case: s=>//= x s; apply/sub_path/subrel_ord. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)