proposition: Lemma worders_qle_prop4 E: (worders_quo E) <=s E -> False.
proof: Proof. move => [f [injf sf tf]]. move:(Imf_Starget (proj1 injf)); rewrite tf; set G := Imf f => sGE. move:(restriction_to_image_fb injf); set g := restriction_to_image f => bg. have bgp: bijection_prop g (worders_quo E) G. by split => //; rewrite /g/restriction_to_image/restriction2; aw. have srQ := (proj2 (worders_qle_order E)). move: (conj (worders_qle_prop3 E) srQ) => H. move:(worder_transportation H bgp) => [r wor is1]. have rw: inc r (worders E) by apply/wordersP; exists G => //; split => //; ue. 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. have Xsr2: inc X (substrate (worders_order E)) by ue. move: (worders_qle_prop2 xq rX) => is2. case: (segment_not_iso (worders_qle_prop3 E) Xsr2); exact: (orderIT is1 is2). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)