proposition: Lemma worders_qle_prop3 E: worder (worders_order E).
proof: Proof. move: (worders_qle_order E) =>[or sr]. move:(worders_eq_equivalence E) => ee. apply: (worder_prop_rev or) => T; rewrite sr => Tsr [X xT]. move:(Tsr _ xT) => Xq. move:(setQ_ne ee Xq) =>[a aX]. move:(worders_qle_prop2 Xq aX) => is1; set Z := segment (worders_order E) X. pose T0 := T\cap Z. have zp x: inc x (worders_quo E) -> inc x Z \/ gle (worders_order E) X x. move => xq; move:(xq) => xq1; rewrite - sr in Xq xq. case: (total_order_pr2 (worders_qle_total E) xq Xq) => lt; last by right. by left; apply/segmentP. case: (emptyset_dichot T0) => te. ex_tac => b bt; case: (zp _ ((Tsr _ bt))) => // bZ. by empty_tac1 b; apply: setI2_i. move: (orderIS is1) =>[f fiso]. have aux: sub Z (substrate (worders_order E)) by apply: sub_segment. move:fiso =>[oa ob]; rewrite (iorder_sr or aux); move => [bf sf tf] ffi. have sub1: sub T0 (source f) by rewrite sf; move => t /setI2_P[]. have ff := (proj1 (proj1 bf)). move:(Vf_image_P ff sub1) => vfsP. have sub2: sub (Vfs f T0) (substrate a). by rewrite - tf; apply: fun_image_Starget1. have nee: nonempty (Vfs f T0) by apply:(nonempty_image ff te sub1). move:(worders_quo_isr Xq aX) => aw. move:(worders_wor aw) => woa. move:(worder_prop woa sub2 nee) =>[b /vfsP [Y /setI2_P [yY yZ] uv] bl]; ex_tac. move => C cT. move/Zo_P: (yZ)=> [two [mt1 nxy]]. case: (zp _ ((Tsr _ cT))) => cZ; last by order_tac. move: (setI2_i cT cZ) => ct0. have /bl: inc (Vf f C) (Vfs f T0) by apply/vfsP; ex_tac. rewrite - sf in yZ cZ. by rewrite uv; move/(ffi Y C yZ cZ) => /iorder_gleP; case. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)