proposition: Lemma worders_qle_prop5 E: (exists f, injection_prop f E (worders_quo E)) <-> (exists r, worder_on r E).
proof: Proof. move: (worders_qle_order E) =>[orQ srQ]. split. move=>[f ff];apply:(wor_from_injection (conj (worders_qle_prop3 E)srQ) ff). move => [r wor]; move: (proj2 wor) => sr. have rw: inc r (worders E) by apply/wordersP; exists E => //. move:(worders_eq_equivalence E) => ee. have xsrr: inc r (substrate (worders_eq E)) by rewrite worders_eq_sr. set X := class (worders_eq E)r. have xq: inc X (worders_quo E) by apply: inc_class_setQ. have rX: inc r X by apply: inc_itself_class. move: (worders_qle_prop2 xq rX) => [f [ _ _ is2 _]]. move:(is2) =>[[[ff ii ] _] sf tf]. exists (Lf (Vf f) E (worders_quo E)); saw. have sz1: sub (target f) (worders_quo E). by rewrite tf (proj2 (seg_order_osr X orQ)) - srQ; apply: sub_segment. rewrite - {1} sr - sf; apply: lf_injective. move => t te; apply: sz1; Wtac. by move => u v iE vE; apply: ii. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)