proposition: Lemma total_order_small r: order r -> small_set (substrate r) -> total_order r.
proof: Proof. move=> or ss; split=>// x y xs ys; rewrite (ss _ _ xs ys). by left; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)