proposition: Lemma compose_order_morphism r r' r'' f f': order_morphism f r r' -> order_morphism f' r' r'' -> order_morphism (f' \co f) r r''.
proof: Proof. move=>[or or' [ff sf tf] fp][_ or'' [ff' sf' tf'] fp']. have cff': f' \coP f by split => //; rewrite sf'. split => //; first by saw;fct_tac. hnf; aw; move=> x y xsf ysf; rewrite !compfV //. move: (Vf_target ff xsf)(Vf_target ff ysf); rewrite tf - sf' => xt yt. split; first by move => h; apply /(fp' _ _ xt yt) /(fp _ _ xsf ysf). by move/(fp' _ _ xt yt) /(fp _ _ xsf ysf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)