proposition: Lemma noid_prop1 (M:= noid_E) (g := noid_f): [/\ forall z, inc z r -> restriction2_axioms (Vg f z) (Vg M (Q z)) (Vg M (P z)), forall i j x, gle r i j -> inc x (Vg M j) -> Vf (Vg g (J i j)) x = Vf (Vg f (J i j)) x, forall i, inc i r -> function_prop (Vg g i) (Vg M (Q i)) (Vg M (P i)), forall i j k, gle r i j -> gle r j k -> Vg g (J i j) \co Vg g (J j k) = Vg g (J i k) & forall i, inc i I -> Vg g (J i i) = identity (Vg M i)].
proof: Proof. have rc z: inc z r -> restriction2_axioms (Vg f z) (Vg M (Q z)) (Vg M (P z)). move => zr. move:(function_f zr) =>[ff sf tf]. move: (pr1_sr zr)(pr2_sr zr); rewrite substrate_r => iI jI. move:(noid_prop0 jI); rewrite /M /noid_E ! LgV// - sf => hu. split. - done. - done. - rewrite tf; move:(noid_prop0 iI); rewrite /noid_E LgV//. - have pz:= ((proj31 preorder_r) _ zr). move => t /(Vf_image_P ff hu) [u uif ->]. move:(zr); rewrite - pz => zr'. have ii: inc (J(P z) (P z)) r by apply: (proj32 preorder_r (P z)); rewrite substrate_r. have jj: inc (J(Q z) (Q z)) r by apply: (proj32 preorder_r (Q z)); rewrite substrate_r. case:(function_f ii); aw => fii sii tii. case:(function_f jj); aw => fjj sjj tjj. have co1: Vg f z \coP Vg f (J (Q z) (Q z)) by split => //; ue. have co2: Vg f (J (P z) (P z)) \coP Vg f z by split => //; ue. move/(Imf_P fjj):uif => [v]; rewrite sjj => vej vv. apply/(Imf_P fii); rewrite sii vv. exists (Vf (Vg f z) v); first Wtac. move:(compose_f ii zr') (compose_f zr' jj); rewrite pz => eqa eqb. move:(f_equal (Vf ^~ v) eqa)(f_equal (Vf ^~ v) eqb). rewrite !compfV //; try ue; move => -> //. have rd:forall i j x, gle r i j -> inc x (Vg M j) -> Vf (Vg g (J i j)) x = Vf (Vg f (J i j)) x. move => i j x lij xm. have hb':inc x (Vg M (Q (J i j))) by aw. rewrite /g /noid_f -(restriction2_V (rc _ lij) hb'); rewrite LgV//. have re i: inc i r -> function_prop (Vg g i) (Vg M (Q i)) (Vg M (P i)). move => ir; rewrite /g/noid_f LgV//. exact: (restriction2_prop (rc _ ir)). have rg i: inc i I -> Vg g (J i i) = identity (Vg M i). move => iI. have ii: inc (J i i) r by apply: (proj32 preorder_r i); rewrite substrate_r. move:(compose_f ii ii) => cc. move:(function_f ii); aw; move => [ff sf tf]. move:(re _ ii); aw => fp; apply: (identity_prop0 fp) => x xM. rewrite (rd _ _ _ ii xM). move:xM; rewrite /M /noid_E LgV//; move/(Imf_P ff); rewrite sf. move => [u uE ->]; rewrite - {3}cc; rewrite compfV //; [ split => //; ue | ue ]. split => // i j k lij ljk. have lik: gle r i k by apply: (proj33 preorder_r) lij ljk. move: (re _ lij) => [fij sij tij]. move: (re _ ljk) => [fjk sjk tjk]. move: (re _ lik) => [fik sik tik]. rewrite ! pr1_pair in tij tik tjk. rewrite ! pr2_pair in sij sik sjk. have co1: Vg g (J i j) \coP Vg g (J j k) by split => //; rewrite sij tjk. have fc1: function (Vg g (J i j) \co Vg g (J j k)) by apply: compf_f. apply: function_exten => //. - by aw; rewrite sik sjk. - by aw; rewrite tij tik. aw; rewrite sjk => x xM. have cpp: Vg f (J i j) \coP Vg f (J j k). move: (function_f lij) => [fa fb fc]. move: (function_f ljk) => [fa' fb' fc']. by split => //; rewrite fb fc'; aw. have vm: inc (Vf (Vg g (J j k)) x) (Vg M j). by rewrite - tjk; apply:(Vf_target fjk); rewrite sjk. have xM': inc x (source (Vg f (J j k))). have kI: inc k I by rewrite - substrate_r; order_tac. move: (function_f ljk) => [_ -> _]; aw. by apply:(noid_prop0 kI). have xM'': inc x (source (Vg g (J j k))) by rewrite sjk. rewrite (rd _ _ _ lik xM) - (compose_f lij ljk). by rewrite !compfV //(rd _ _ _ lij vm) (rd _ _ _ ljk xM). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)