proposition: Lemma ordP x y : total_spec x y (ord x y) (x == y) (ord y x).
proof: Proof. case H1: (x == y). - by rewrite (eqP H1) irr; apply: total_spec_eq. case H2: (ord x y); case H3: (ord y x). - by case: (nsym H2 H3). - by apply: total_spec_lt H2. - by apply: total_spec_gt H3. by move: (ord_total x y); rewrite H1 H2 H3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)