proposition: Lemma order_morphism_increasing f r r': order_morphism f r r' -> strict_increasing_fun f r r'.
proof: Proof. move => h; move: (order_morphism_sincr h) => si. move:h=> [or or' [ ff sr sr'] rel]; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)