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