proposition: Lemma order_leT a b c: a <=O b -> b <=O c -> a <=O c.
proof: Proof. move =>[oa ob [f [x [xsb is1]]]] [_ oc [g [y [ysc is2]]]]. move: (iorder_osr ob xsb) =>[or2 sr2]. move: (iorder_osr oc ysc) =>[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 sxg: sub x (source g) by ue. have ff: function f by fct_tac. move:(@fun_image_Starget1 g fg x); rewrite tg; set z:= Vfs g x => zy. move:(sub_trans zy ysc) => zsc. move:(iorder_osr oc zsc) =>[or4 /esym 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 sxg); exists (Vf f t) => //; Wtac. split => //; exists (Lf h (substrate a) z) , z; split => //; split=> //. hnf; saw; apply: lf_bijective. - done. - hnf; rewrite - sf; move => u v usr vsr ee. apply:(proj2(proj1 bf) _ _ usr vsr); apply: ig => //; apply: sxg; Wtac. - move => t /(Vf_image_P fg sxg) [u ux ->]. move:(proj2(proj2 bf)); rewrite tf => hh; move:(hh u ux); rewrite sf. by move =>[v vv ->]; exists v. hnf; aw; move => u v usr vsr; rewrite !LfV //. move:(ax _ usr)(ax _ vsr) => uz vz. rewrite - sf in usr vsr. apply: (iff_trans(fiso u v usr vsr)). have fux: inc (Vf f u) x by Wtac. have fvx: inc (Vf f v) x by Wtac. move:(sxg _ fux) (sxg _ fvx) => fus fvs. apply:(iff_trans (iff_trans (iorder_gle0P b fux fvx) (giso _ _ fus fvs))). apply: (iff_trans (iorder_gle0P c (zy _ uz) (zy _ vz))). exact (iff_sym (iorder_gle0P c uz vz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)