proposition: Lemma trans_ords : transitive ords.
proof: Proof. elim=>[|y ys IHy][|x xs][|z zs]//=. case:eqP=>//[->|H0];case:eqP=>//H; first by move/IHy; apply. - by case:eqP=>//; rewrite -H; first (by move/H0). case:eqP=>//[->|H1] H2; first by move/(nsym H2). by move/(trans H2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)