proposition: Lemma order_le_transitive x y z: x <=O y -> y <=O z -> x <=O z.
proof: Proof. move=> [ox oy [f [y1 [pa pb]]]] [_ oz [g [z1 [pc pd]]]]. split => //. move: pb => [orx oix [[[ff injf] sjf] sf tf] etcf]. move: pd => [ory oiy [[[fg injg] sjg] sg tg] etcg]. move: tf tg; rewrite ! iorder_sr// => tf tg. set z2:= Vfs g y1. have y1sg: sub y1 (source g) by ue. have sz2z1: sub z2 z1 by rewrite - tg /z2; apply: fun_image_Starget1. have sz2: sub z2 (substrate z) by apply: (sub_trans sz2z1). set h:= Lf (fun t => (Vf g (Vf f t))) (substrate x) z2. have ta: lf_axiom (fun t => Vf g(Vf f t)) (substrate x) z2. rewrite - sf;move=> t rx; apply /(Vf_image_P fg y1sg). exists (Vf f t) => //; Wtac. move: (iorder_osr oz sz2) => [pa1 pb1]. exists h; exists z2; split => //; rewrite /h; split;fprops. rewrite pb1;saw;apply: lf_bijective => //. rewrite - sf => u v ux vx sw; apply: injf => //. apply: injg =>//; rewrite sg; apply: pa; rewrite - tf;Wtac. move=> u /(Vf_image_P fg y1sg) [a ay1] ->. move: ay1; rewrite - tf => af; move: ((proj2 sjf) _ af). move=> [b bsf ->]; exists b => //; ue. red; aw;move => a b asf bsf; rewrite !LfV //. move: (ta _ asf) (ta _ bsf) => ta1 ta2. rewrite - sf in asf bsf. have wa: inc (Vf f a) y1 by rewrite - tf; Wtac. have wb: inc (Vf f b) y1 by rewrite - tf; Wtac. have wa1: inc (Vf f a) (source g) by ue. have wb1: inc (Vf f b) (source g) by ue. set H1 := (etcf _ _ asf bsf); set Hb := (etcg _ _ wa1 wb1). split. move /H1 => p1; apply /iorder_gle0P => //. move: (iorder_gle1 p1); move /Hb => p2; exact :(iorder_gle1 p2). move => p2; apply /H1;apply /iorder_gle0P => //; apply /Hb. move: (iorder_gle1 p2) => p1. by apply /iorder_gle0P => //; apply: sz2z1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)