proposition: Lemma order_isomorphism_incr f r r': order_isomorphism f r r' -> fincr_prop f r r'.
proof: Proof. by move => h; apply: order_morphism_incr; apply:order_isomorphism_w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)