proposition: Lemma total_order_pr2 r x y: total_order r -> inc x (substrate r) -> inc y (substrate r) -> (glt r x y \/ gle r y x).
proof: Proof. move=> tor xs ys. move: tor=> [_ p]; rewrite /glt; case: (p _ _ xs ys); last by right. by case: (equal_or_not x y); [ move=> ->; right | left]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)