proposition: Lemma worders_qle_prop6 E (Z := Zo (worders_quo E) (fun z => exists2 y, inc y z & substrate y \Eq E)) (X := the_least (induced_order (worders_order E) Z)) (Y := seg_order (worders_order E) X): (exists f, injection_prop f E (worders_quo E)) -> worder Y /\ substrate Y \Eq E.
proof: Proof. move /worders_qle_prop5 => [r wor]; move: (proj2 wor) => sr. have rw: inc r (worders E) by apply/wordersP; exists E => //. move:(worders_eq_equivalence E) => ee. move: (worders_qle_order E) =>[orQ srQ]. have xsrr: inc r (substrate (worders_eq E)) by rewrite worders_eq_sr. set C := class (worders_eq E) r. have cq: inc C (worders_quo E) by apply: inc_class_setQ. have CZ: inc C Z. apply: (Zo_i cq); exists r; first by apply:inc_itself_class. rewrite (proj2 wor); apply: EqR. have nez: nonempty Z by ex_tac. have zs: sub Z (substrate (worders_order E)). rewrite srQ; apply: Zo_S. move:(iorder_osr orQ zs) =>[or1 sr1]. move: (worders_qle_prop3 E) => woQ. split; first by apply: (seg_order_wor _ woQ). move: (proj1(the_least_pr or1 (proj2 woQ _ zs nez))). rewrite sr1; move => /Zo_P [Xq [a aX etc]]. move: (worders_qle_prop2 Xq aX) =>[f [_ _ bf _]]. have eq1: (substrate a) \Eq substrate Y by exists f. exact: (EqT (EqS eq1) etc). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)