proposition: Lemma compose_order_is r r' r'' f f': order_isomorphism f r r' -> order_isomorphism f' r' r'' -> order_isomorphism (f' \co f) r r''.
proof: Proof. move => pa pb; move: (order_isomorphism_w pa) (order_isomorphism_w pb) => h1 h2. apply: order_isomorphism_ws (compose_order_morphism h1 h2). move: pa pb =>[_ _ [bf sf tf] _][_ _ [bf' sf' tf'] _]. by apply: compose_fb => //; split => // ; try fct_tac; rewrite sf'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)