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