proposition: Lemma worders_qle_prop2 E X a: inc X (worders_quo E) -> inc a X -> a \Is (seg_order (worders_order E) X).
proof: Proof. move => Xq ax. move:(worders_eq_equivalence E) => ee. move: (worders_qle_order E) =>[wor sr]. set Z := segment (worders_order E) X. move:(worders_quo_isr Xq ax) => aw. move:(worders_wor aw) => woa; move: (proj1 woa) => oa. pose ios c := seg_order a c. have hb x b: inc x Z -> inc b x -> exists2 c, inc c (substrate a) & b \Is ios c. move => /segmentP [/graph_on_P1 [xq _ lex] nexx] ibx. move:(worders_qle_prop lex ibx ax) => lba. move:(worders_quo_isr xq ibx) => bw. move:(worders_wor bw) => wob. move/(compare_wor_prop wob woa): lba =>[_ _ [y ysb [f is1]]]. case:(well_ordered_segment woa ysb). move => ysa; move: is1; rewrite ysa (iorder_substrate (proj1 woa)) => is1. have ba: b \Is a by exists f. case: nexx; exact:(worders_quo_prop xq Xq ibx ax ba). by move => [c csr cv]; exists c => //; rewrite /ios/seg_order - cv; exists f. have hc' c: inc c (substrate a) -> inc (ios c) (worders E). move/wordersP: aw => [F sFE [_ sra]]. move => csa; apply/wordersP. move: (@sub_segment a c) => s1. have ss: sub (segment a c) E by apply:sub_trans sFE; rewrite - sra. by exists (segment a c) => //; apply:(seg_order_wosr). have hc c: inc c (substrate a) -> inc (ios c) (substrate (worders_eq E)). by rewrite worders_eq_sr; apply: hc'. have hd c: inc c (substrate a) -> inc (class (worders_eq E) (ios c)) Z. move => cs; move: (hc _ cs) => ccs; apply/segmentP. move: (inc_itself_class ee ccs) => iic. split. have ra:= (inc_class_setQ ccs). apply/graph_on_P1; split => //; split => //. move: (@sub_segment a c) => s1. exists (ios c), a; split => //. move:(seg_order_osr c oa) =>[or1 sr1]. split => //;exists (identity (segment a c)), (segment a c); split => //. by rewrite -{1} sr1; apply: (identity_is or1). move => sv. move: ax; rewrite - sv; move=> /(class_P ee) /graph_on_P1 [ra _ /orderIS rc]. apply: (segment_not_iso woa cs rc). have he: sub Z (substrate (worders_order E)) by apply: sub_segment. move:(iorder_osr wor he) =>[ orE srE]. pose f := Lf (fun c => (class (worders_eq E) (ios c))) (substrate a) Z. exists f; split => //. rewrite /f; hnf; aw; split => //. apply: lf_bijective. - exact. - move => u v usa vsa scl. move:(hc _ vsa) => ta. have: related (worders_eq E) (ios u )(ios v). by apply/(class_P ee); rewrite scl; apply: (inc_itself_class ee). move/graph_on_P1 =>[tb tc td]. exact:(iso_unique_segment woa usa vsa td). - move => y yZ. move: (he _ yZ); rewrite sr => yq; move:(setQ_ne ee yq) => [b iby]. move:(hb _ _ yZ iby) =>[c csr cc]; ex_tac. move:(hc' c csr) (worders_quo_isr yq iby)=> ics ibs. rewrite (worder_in_class_pr yq iby); apply: (class_eq1 ee). by apply/graph_on_P1. rewrite /f; hnf; aw;trivial; move => u v usa vsa; rewrite !LfV//. move:(hd _ usa)(hd _ vsa) => cus cvs. move:(hc' _ usa)(hc' _ vsa) => iuE ivE. apply: iff_trans (iff_sym (iorder_gle0P (worders_order E) cus cvs)). apply: iff_trans (worders_qle_propc iuE ivE). have tb: sub (segment a v) (substrate a) by apply: sub_segment. move:(seg_order_osr u oa) =>[or1 tc]. move:(seg_order_osr v oa) =>[or2 td]. split => lr1. have ra: sub (segment a u) (segment a v) by apply: segment_monotone. have te: sub (segment a u) (substrate a) by apply: sub_segment. split => //;exists (identity (segment a u)), (segment a u). rewrite -{2} tc td; split => //; rewrite (iorder_trans _ ra). by apply: (identity_is (proj1 (iorder_osr oa te))). move/(compare_wor_prop (worders_wor iuE) (worders_wor ivE)): lr1. move =>[ _ _ [x xs is1]]. move:(proj1 xs); rewrite td => sxg. move: is1; rewrite /ios (iorder_trans _ sxg). have [w le2 ->]: exists2 w, gle a w v & x = segment a w. case: (well_ordered_segment (worders_wor ivE) xs); rewrite td. by move ->; exists v => //; order_tac. move => [w /segmentP ll ->]; exists w. exact: (proj1 ll). by rewrite segment_induced. by move /(iso_unique_segment woa usa (arg1_sr le2)) => ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)