proposition: Lemma oantisym : antisymmetric (@oleq T).
proof: Proof. move=>x y; rewrite /oleq (eq_sym x). case: eqP=>// _; rewrite !orbF=>/andP [H1 H2]. by move: (trans H1 H2); rewrite irr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)