proposition: Lemma order_morphism_incr f r r': order_morphism f r r' -> fincr_prop f r r'.
proof: Proof. move => [or or' [ff sf tf] h] x y rxy. have xsr: inc x (source f) by rewrite sf; order_tac. have ysr: inc y (source f) by rewrite sf; order_tac. by move/(h _ _ xsr ysr):rxy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)