proposition: Lemma order_morphism_siso f r r': order_morphism f r r' -> fsiso_prop f r r'.
proof: Proof. move => h x y xsf ysf; split; first by apply :order_morphism_sincr. have fi :=(order_morphism_fi h). have [or or' [ff sf tf] hp] := h. by move => [pa pb]; split; [ apply /hp | move => h1; case: pb; rewrite h1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)