proposition: Lemma total_order_morphism f r r': total_order r -> order r' -> injection f -> substrate r = source f -> substrate r' = target f -> {inc source f &, fincr_prop f r r'} -> order_morphism f r r'.
proof: Proof. move=> to or' [ff injf] sf tf incf. apply: total_order_increasing_morphism => //. move: to => [or _]; split => // x y [lexy nxy]. move:(arg1_sr lexy)(arg2_sr lexy); rewrite sf => xsf ysf. by split; [apply: incf | dneg aa; apply: injf]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)