proposition: Lemma oleq_ord_trans (n m p : T) : oleq m n -> ord n p -> ord m p.
proof: Proof. by case/orP; [apply: trans | move/eqP=>->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)