proposition: Lemma wor_from_injection E Q r f: worder_on r Q -> injection_prop f E Q -> (exists r, worder_on r E).
proof: Proof. move => [wor sr] [[ff injf] sf tf]. move: (proj1 wor) => or. pose cp x y := gle r (Vf f x) (Vf f y). have rre a: inc a E -> cp a a. move => ae; rewrite /cp; order_tac; rewrite sr; Wtac. set s := graph_on cp E. have srE: substrate s = E by rewrite graph_on_sr. have os: order s. rewrite/s/cp;apply: order_from_rel1. - move => y x z /= ha hb; order_tac. - move => x y xE yE l1 l2. have: (Vf f x) = (Vf f y) by order_tac. apply: injf; ue. - done. exists s; split => //; apply:(worder_prop_rev os) => x xE xnE. set A := fun_image x (Vf f). have neA: nonempty A by apply: funI_setne. have sas: sub A (substrate r). by rewrite sr =>t /funI_P [j jx ->]; Wtac; rewrite sf - srE; apply: xE. move: (worder_prop wor sas neA) =>[a aA al]. move/funI_P: aA => [u ue uv]; ex_tac => b bx. move:(xE _ ue)(xE _ bx) ; rewrite srE => qa qb. apply /graph_on_P1; split => //. rewrite /cp; rewrite - uv; apply: al. apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)