proposition: Lemma order_le_alt4 r r': r <=O r' -> (exists f, order_morphism f r r').
proof: Proof. move=> [o1 o2 [f [z [sr [oa ob [[ [ff injf] sjf] sf tf] etc]]]]]. move: tf; rewrite iorder_sr // => tf. have ta: lf_axiom (Vf f) (substrate r) (substrate r'). rewrite - sf; move=> t tsf; apply: sr; Wtac. exists (Lf (Vf f) (substrate r) (substrate r')). split => //;first saw. by apply: lf_function. red; aw;move=> x y xsr ysr; rewrite ! LfV//;rewrite - sf in xsr ysr. split => h; first by move/(etc _ _ xsr ysr): h => t; exact (iorder_gle1 t). apply /(etc _ _ xsr ysr); apply /iorder_gle0P => //; Wtac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)