proposition: Lemma total_order_pr1 r x y: total_order r -> inc x (substrate r) -> inc y (substrate r) -> [\/ glt r x y, glt r y x | x = y ].
proof: Proof. move=> [_ p] xs ys. case: (equal_or_not x y); [by constructor 3 | move => xy]. rewrite /glt; case:(p _ _ xs ys); [constructor 1 | constructor 2]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)