proposition: Lemma total_ordf : forall x y, [|| ordf x y, x == y | ordf y x].
proof: Proof. move=>x y; rewrite /ordf; case: ltngtP=>//= H; rewrite ?orbT ?orbF //. have [H1 H2]: x \in enum T /\ y \in enum T by rewrite !mem_enum. by rewrite -(nth_index x H1) -(nth_index x H2) H eq_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq fintype)