proposition: Lemma prl_ne2_sigma_maximal_prop2 A: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> pr1_ne2_hyp3_weak -> maximal prl_ne2_sigma_order A -> (forall i, inc i (psI S) -> singletonp (Vg A i)).
proof: Proof. move => Hi Hii mA i iI. move: prl_ne2_sigma_osr =>[or sr]. move: (mA) => []; rewrite sr => As amax. move/Zo_P:(As) => [/setXb_P[dgA dA vA] [pA qA]]. rewrite FS_domain in vA. move:(Hii i (Vg A i) iI (vA _ iI) (pA _ iI)) => [xi xia xib']. pose II j := (Vfi1 (Vg (psf S) (J i j)) xi). have xib: forall j, gle (psr S) i j -> inc (II j) (Vg FS_fam j). by move: xib'; rewrite /pr1_ne2_hyp3_aux. set B := Lg (psI S)(fun j => Yo (gle (psr S) i j)(Vg A j \cap (II j)) (Vg A j)). have ra: inc B (productb FS_fam). rewrite/B;apply/setXb_P; rewrite FS_domain;split; aww => j jI. rewrite LgV//. move: (vA _ jI) => ha; Ytac hh => //; apply: (FS_inter jI). move => t /set2_P; case => ->; fprops. apply: set2_ne. have Ha j : gle (psr S) i j -> forall x, inc x (II j) <-> inc x (Vg (psE S) j) /\ xi = Vf (Vg (psf S) (J i j)) x. move => lij x. case: (ps_function_f lij); aw => ff sf tf. by rewrite /II; move:(iim_fun_set1_P xi ff); rewrite sf. have rb: (forall j, inc j (psI S) -> nonempty (Vg B j)). rewrite /B;move => j jI; rewrite LgV//; Ytac lij; last by apply: pA. move:(xia); rewrite (prl_ne2_sigma_maximal_prop1 Hi mA lij). case: (ps_function_f lij); aw => ff sf tf. have hd: sub (Vg A j) (Vg (psE S) j). by apply/setP_P; apply:(FS_range jI); apply:vA. have hc: sub (Vg A j) (source (Vg (psf S) (J i j))) by ue. move /(Vf_image_P ff hc) => [u ua ub]; exists u; apply/setI2_P; split => //. by apply/(Ha _ lij); split => //; apply: hd. have BS_sigma: inc B prl_ne2_sigma. apply/Zo_P; split=> //; split => // j k lejk. move:(prl_prop0 lejk) => [jI kI]. rewrite/B ! LgV//. case: (ps_function_f lejk); aw => fjk sjk tjk. have hd: sub (Vg A k) (source (Vg (psf S) (J j k))). by rewrite sjk; apply/setP_P; apply:(FS_range kI); apply:vA. case: (p_or_not_p (gle (psr S) i j)) => leij; Ytac0. move:(proj33 (ps_preorder_r S) _ _ _ leij lejk) => leik. Ytac0. have ha: sub (Vg A k \cap II k) (source (Vg (psf S) (J j k))). apply: (sub_trans (@setI2_1 (Vg A k) (II k)) hd). move => t /(Vf_image_P fjk ha) [u /setI2_P [ua ub] ->]. apply/setI2_P; split. apply: (qA _ _ lejk); apply/(Vf_image_P fjk hd); ex_tac. move/(Ha _ leik): ub => [uE xb]; apply/(Ha _ leij); split; first Wtac. by rewrite (prl_prop3 leij lejk uE). move => t ta; apply:(qA _ _ lejk);apply/(Vf_image_P fjk hd). have hb: sub (Yo (gle (psr S) i k) (Vg A k \cap II k) (Vg A k)) (Vg A k). Ytac hx; fprops; apply: setI2_1. move /(Vf_image_P fjk (sub_trans hb hd) ): ta => [u ua ->]; exists u; fprops. have cp1: gle prl_ne2_sigma_order A B. apply/graph_on_P1; split => // j jI; rewrite /B LgV//. Ytac hx; fprops; apply: setI2_1. apply/singletonP; split; first ex_tac. have lii:= (prl_prop1 iI). rewrite - (amax _ cp1) /B (LgV iI) (Y_true lii). move => a b /setI2_P [ha /(Ha _ lii) [hb hc]] /setI2_P [qa /(Ha _ lii) [qb qc]]. by move:hc qc; rewrite (ps_identity_f iI) !idV // => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)