proposition: Lemma order_morphism_sincr f r r': order_morphism f r r' -> fsincr_prop f r r'.
proof: Proof. move => h; move: (order_morphism_fi h) => fi. move: h => [or or' [ff sf tf] h] x y [rxy nxy]. have xsr: inc x (source f) by rewrite sf; order_tac. have ysr: inc y (source f) by rewrite sf; order_tac. split; first by move/(h _ _ xsr ysr):rxy. by dneg aux; apply: (proj2 fi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)