proposition: Lemma ord_total x y : [|| ord x y, x == y | ord y x].
proof: Proof. case E: (x == y)=>/=; first by rewrite orbT. by apply: semiconnex; rewrite negbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)