proposition: Lemma order_le_worA a b: worder a -> worder b -> a <=O b -> b <=O a -> a \Is b.
proof: Proof. move => woa wob. move: (proj1 woa)(proj1 wob) => oa ob. move/(compare_wor_prop woa wob) =>[_ _ [y ysb [f is1]]]. move/(compare_wor_prop wob woa) =>[_ _ [x xsa [g is2]]]. move:(proj1 ysb) (proj1 xsa) => syb sxa. move: (iorder_osr ob syb) =>[or2 sr2]. move: (iorder_osr oa sxa) =>[or3 sr3]. move:is1 =>[_ _ [bf sf tf] fiso ]; rewrite sr2 in tf. move:(is2) =>[_ _ [[[fg ig][_ sgg]] sg tg] giso ]; rewrite sr3 in tg. have syg: sub y (source g) by ue. have ff: function f by fct_tac. move:(@fun_image_Starget1 g fg y); rewrite tg; set z:= Vfs g y => zx. move:(sub_trans zx sxa) => zsc. move:(iorder_osr oa zsc) =>[or4 sr4]. pose h := (fun t => Vf g (Vf f t)). have ax': lf_axiom h (substrate a) z. move => t tsx /=; apply/(Vf_image_P fg syg); exists (Vf f t) => //; Wtac. have ax: lf_axiom h (substrate a) (substrate a) by move => t /ax' /zsc. pose h1 := (Lf h (substrate a) (substrate a)). have hinj: injection h1. apply: lf_injective => //; rewrite /h1. hnf; rewrite - sf; move => u v usr vsr ee. apply:(proj2(proj1 bf) _ _ usr vsr); apply: ig => //; apply: syg; Wtac. have pd: order_morphism h1 a a. apply:(total_order_morphism (worder_total woa) oa hinj). - by rewrite /h1; aw. - by rewrite /h1; aw. - rewrite /h1; aw => u v usr vsr; rewrite !LfV// => leab. rewrite - sf in usr vsr. have fux: inc (Vf f u) (source g) by apply: syg; Wtac. have fvx: inc (Vf f v) (source g) by apply: syg; Wtac. move/(fiso u v usr vsr): leab => /iorder_gle1 ll. by move/(giso _ _ fux fvx) : ll => /iorder_gle1. have pc: segmentp a (Imf h1). have fh: function h1 by fct_tac. have th: target h1 = (substrate a) by rewrite /h1; aw. have sh: source h1 = (substrate a) by rewrite /h1; aw. split; first by rewrite - th; apply: Imf_Starget. move => u v /(Imf_P fh) [u1 u1h ->]; rewrite /h1. rewrite sh in u1h; rewrite LfV// => le1. have ha: inc (Vf f u1) (source g) by apply: syg; Wtac. have hb: inc (h u1) x by rewrite /h; Wtac. move:(proj2 xsa _ _ hb le1) => vx. have hc: inc v (target g) by ue. move: (sgg _ hc) =>[v1 v1sg v1v]. have hd: inc (Vf f u1) (source g) by apply: syg; Wtac. have he: inc (Vf g v1) x by ue. have hf: gle (induced_order a x) (Vf g v1) (Vf g (Vf f u1)). apply/iorder_gleP; split => //; ue. move/(giso v1 (Vf f u1) v1sg hd): hf => le3. have hi: inc (Vf f u1) y by Wtac. move:(proj2 ysb (Vf f u1) v1 hi le3) => v1y. have hc': inc v1 (target f) by ue. move: ((proj2 (proj2 bf)) _ hc') =>[v2 v2sg v2v]. apply/(Imf_P fh); exists v2; first by rewrite sh - sf. have hk: inc v2 (substrate a) by ue. by rewrite /h1 LfV//; rewrite /h - v2v. move:(unique_isomorphism_onto_segment woa pc pd) => hi. move: is2. have ->: x = substrate a. apply: extensionality => // t tb. move: (f_equal (Vf ^~t) hi); rewrite idV ///h1 LfV// => <-. rewrite /h; Wtac; apply: syg; Wtac. by rewrite (iorder_substrate oa) => ok; apply:orderIS; exists g. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)