proposition: Lemma prl_ne2_sigma_maximal_prop1 A: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> maximal prl_ne2_sigma_order A -> (forall i j, gle (psr S) i j -> (Vg A i) = Vfs (Vg (psf S) (J i j)) (Vg A j)).
proof: Proof. move: prl_ne2_sigma_osr =>[or sr] H. move => []; rewrite sr => As amax. move/Zo_P:(As) => [ /setXb_P [fgA dA rA] [Ap1 Ap2]]. have Hd i: inc i (psI S) -> sub (Vg A i) (Vg (psE S) i). move => iI; apply/setP_P; apply:(FS_range iI); apply: rA; ue. pose inta i:= Zo (psI S) (fun j => gle (psr S) i j). pose II i j := Vfs (Vg (psf S) (J i j)) (Vg A j). pose B := Lg (psI S) (fun i => intersectionf (inta i) (II i)). pose rri i := range (Lg (inta i) (II i)). have Ha i:inc i (psI S) -> nonempty (inta i). by move => iI; exists i; apply/Zo_P; split => //; apply: prl_prop1. have Hb i: inc i (psI S) -> nonempty (rri i). move => iI;apply: (nonempty_range _ (Ha i iI)). have ra i: inc i (psI S) -> sub (rri i) (Vg FS_fam i). move => iI t /Lg_range_P [j /Zo_P [jI leij] ->]. apply:(FS_prop_iv leij); apply: rA; ue. have rb: inc B (productb FS_fam). rewrite/B; apply/setXb_P; split; aww; rewrite FS_domain. move=> i iI;rewrite LgV //setIf_alt; apply:(FS_inter iI (ra _ iI) (Hb _ iI)). have rc i j k: gle (psr S) i j -> gle (psr S) j k -> sub (II i k) (II i j). move => lij ljk. rewrite /II - (ps_compose_f lij ljk). case: (prl_prop4 ljk) => fjk sjk tjk. move: (prl_prop2 lij ljk) => coP. move: (arg2_sr ljk); rewrite ps_substrate_r => /Hd hb. move => t/(Vf_image_P (compf_f coP));aw; rewrite sjk => ha. move:(ha hb) => [u uak ->]; rewrite compfV//; last by rewrite sjk; apply: hb. case: (prl_prop4 lij) => fij sij tij. move: (arg1_sr ljk); rewrite ps_substrate_r => /Hd; rewrite - sij => hd. apply/(Vf_image_P fij hd);exists (Vf (Vg (psf S) (J j k)) u) => //. apply:(Ap2 _ _ ljk); apply/(Vf_image_P fjk); [ by rewrite sjk | ex_tac]. have rd i: inc i (psI S) -> nonempty (Vg B i). rewrite /B;move => iI; rewrite LgV//setIf_alt. apply: (H _ iI _ (ra _ iI) (Hb _ iI)). move/Lg_range_P => [j /Zo_P [jI leij]] se. case: (ps_function_f leij); aw => ff sf _. move: (Ap1 _ jI) => [x xa]. move:(Hd _ jI); rewrite - sf => qa. have /in_set0 //: inc (Vf (Vg (psf S) (J i j)) x) emptyset. rewrite se; apply/(Vf_image_P ff qa); ex_tac. move=> x y /Lg_range_P [j /Zo_P [jI lij] ->] /Lg_range_P[k /Zo_P [kI lik] ->]. move:(rdr (arg2_sr lij) (arg2_sr lik)) => [l [l1 l2]]. exists (II i l); split; try apply: rc => //. apply/Lg_range_P; exists l => //; apply /Zo_P; split => //. by move: (arg2_sr l1); rewrite - ps_substrate_r. apply: (proj33 (ps_preorder_r S) _ _ _ lij l1). have BS_sigma: inc B prl_ne2_sigma. apply/Zo_P; split=> //; split => // i j lij. move: (prl_prop0 lij) => [iI jI]. have ->: Vg B i = intersectionf (inta j) (II i). rewrite /B LgV//; set_extens t. move=> /(setIf_P _ (Ha _ iI)) => hb. apply/(setIf_P _ (Ha _ jI)) => k/Zo_P[ja jb]; apply: hb. by apply/Zo_P; split=> //;apply: (proj33 (ps_preorder_r S) _ _ _ lij jb). move=> /(setIf_P _ (Ha _ jI)) => hb. apply/(setIf_P _ (Ha _ iI)) => k /Zo_P[ kI lik]. move: (rdr (arg2_sr lij) (arg2_sr lik)) => [l [l1 l2]]. have /hb la: inc l (inta j). apply/Zo_P; split => //; rewrite - ps_substrate_r; apply: (arg2_sr l1). exact:((rc _ _ _ lik l2) _ la). case: (prl_prop4 lij) => fij sij tij. have ha: sub (Vg B j) (source (Vg (psf S) (J i j))). rewrite sij; move/setXb_P:rb => [qa qb]; rewrite FS_domain => h. apply/setP_P;apply:(FS_range jI); exact:(h _ jI). move => t /(Vf_image_P fij ha) [u ux -> ]. move: ux; rewrite/B LgV// => /(setIf_P _ (Ha _ jI)) => hb. apply/(setIf_P _ (Ha _ jI)) => [k kk]; move/Zo_P: (kk) => [kI ljk]. case: (prl_prop4 ljk) => fjk sjk tjk. have hc: sub (Vg A k) (source (Vg (psf S) (J j k))) by rewrite sjk; fprops. move/(Vf_image_P fjk hc):(hb _ kk) => [v vA ->]. rewrite (prl_prop3 lij ljk (Hd _ kI _ vA)). case: (ps_function_f (proj33 (ps_preorder_r S) _ _ _ lij ljk)); aw. move => fik sik tik. apply/(Vf_image_P fik); [ rewrite sik ; fprops | ex_tac]. have cp1: gle prl_ne2_sigma_order A B. apply/graph_on_P1; split => // i iI; rewrite /B LgV// => t tI. have iii: inc i (inta i) by apply/Zo_P; split => //; apply: prl_prop1. have ff: function (identity (Vg (psE S) i)) by apply: identity_f. move:(Hd _ iI) => sb; move:(sb); rewrite -(identity_s (Vg (psE S) i)) => sa. move:(ps_identity_f iI) => id. move: (setIf_hi tI iii);rewrite /II id => /(Vf_image_P ff sa). by move => [u ua ->]; rewrite idV//; apply: sb. move => i j lij. move:(prl_prop0 lij) => [iI jI]. have ji: inc j (inta i) by apply/Zo_P. apply: extensionality; last by apply: Ap2. rewrite - {1} (amax _ cp1) /B LgV// => t tI. exact :(setIf_hi tI ji). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)