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