proposition: Lemma order_morphism_fi f r r': order_morphism f r r'-> injection f.
proof: Proof. move => [or or' [ff sf tf] h]. split => // x y xsf ysf sv. have aux: gle r' (Vf f y) (Vf f y) by order_tac; Wtac. apply: (order_antisymmetry or). apply/(h _ _ xsf ysf); ue. apply/(h _ _ ysf xsf); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)