proposition: Lemma noid_prop5f i j k: gle r i j -> gle r j k -> Vg noid_g (J j k) \co Vg noid_g (J i j) = Vg noid_g (J i k).
proof: Proof. move => lij ljk. have lik: gle r i k by apply: (proj33 preorder_r) lij ljk. move: (noid_prop5d lij) => [fij sij tij]. move: (noid_prop5d ljk) => [fjk sjk tjk]. move: (noid_prop5d lik) => [fik sik tik]. rewrite ! pr2_pair in tij tik tjk. rewrite ! pr1_pair in sij sik sjk. have co1: Vg noid_g (J j k) \coP Vg noid_g (J i j). by split => //; rewrite tij sjk. have fc1: function(Vg noid_g (J j k) \co Vg noid_g (J i j)) by apply: compf_f. apply: function_exten => //. by aw; rewrite sij sik. by aw; rewrite tjk tik. aw; rewrite sij => x xM. have xM'':inc x (source (Vg noid_g (J i j))) by rewrite sij. have cpp: Vg f (J j k) \coP Vg f (J i j). move: (function_f lij) => [fa fb fc]. move: (function_f ljk) => [fa' fb' fc']. by split => //; rewrite fb' fc; aw. have xM': inc x (source (Vg f (J i j))). have iI: inc i I by rewrite - substrate_r; order_tac. move: (function_f lij) => [_ -> _]; aw. by apply:(noid_prop5a iI). have : inc (Vf (Vg noid_g (J i j)) x) (Vg noid_E' j). by rewrite - tij; apply:(Vf_target fij); rewrite sij. rewrite (noid_prop5c lij xM) => xM2. rewrite (noid_prop5c lik xM) -(compose_f lij ljk). by rewrite !compfV //(noid_prop5c lij xM) (noid_prop5c ljk xM2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)