proposition: Theorem total_order_monotone_injective f r r': total_order r -> strict_monotone_fun f r r' -> injection f.
proof: Proof. move=> tor. case;move=>[or or' [ff sr sr'] hyp]; split=>// x y; rewrite sr => xs ys sW. by case:(total_order_pr1 tor xs ys) => // /hyp [_]; rewrite sW. by case:(total_order_pr1 tor xs ys) => // /hyp [_]; rewrite sW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)