proposition: Lemma total_lex : forall x y, [|| lex x y, x == y | lex y x].
proof: Proof. move=>[x1 x2][y1 y2]; rewrite /lex /=. case: ifP=>H1. - rewrite (eqP H1) eq_refl -pair_eqE /= eq_refl /=; exact: total. rewrite (eq_sym y1) -pair_eqE /= H1 /=. by move: (total x1 y1); rewrite H1. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq fintype)