proposition: Lemma otrans : transitive (@oleq T).
proof: Proof. move=>x y z /=; case/orP; last by move/eqP=>->. rewrite /oleq; move=>T1; case/orP; first by move/(trans T1)=>->. by move/eqP=><-; rewrite T1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)