proposition: Theorem total_order_increasing_morphism f r r': total_order r -> strict_increasing_fun f r r' -> order_morphism f r r'.
proof: Proof. move=> tor si. have ijf: (injection f) . by apply: (@total_order_monotone_injective f r r') =>//;left. have ic:= (strict_increasing_w si). move: si ic => [or or' [ff sr sr'] sif] [_ _ _ nif]. split => // x y xs ys; split; first by apply: nif. rewrite sr in xs ys. case: (total_order_pr2 tor ys xs) => // h. move: (sif _ _ h)=> p1 p2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)