proposition: Lemma eq_oleq (K : ordType) (x y : K) : (x == y) = oleq x y && oleq y x.
proof: Proof. by rewrite /oleq (eq_sym x); case: ordP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)