proposition: Lemma ord_neq (x y : A) : ord x y -> x != y.
proof: Proof. move=>H; apply/negP=>/eqP E. by rewrite E irr in H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)