proposition: Lemma oleqP x y : oleq_spec x y (oleq x y) (ord y x).
proof: Proof. case:(ordP x y). - by move=>/ordW O; rewrite O; apply: oleq_spec_le. - by move=>/eqP E; rewrite E orefl; apply: oleq_spec_le; apply: orefl. by move=>O; rewrite oleqNord O //=; apply: oleq_spec_gt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)