proposition: Lemma prl_ne2_sigma_inductive: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> inductive prl_ne2_sigma_order.
proof: Proof. move => H. move: prl_ne2_sigma_osr =>[or sr]. move => L; rewrite sr => slS toL. case: (emptyset_dichot L) => Lne. move:(prl_ne2_sigma_ne) => [w we]; exists w; split => //. by rewrite sr. by rewrite Lne;move => x /in_set0. set x := Lg (psI S) (fun i => (intersectionf L (fun z => (Vg z i)))). have Hb i: inc i (psI S) -> sub (range (Lg L (Vg^~ i))) (Vg FS_fam i). move => iI t/ Lg_range_P [l lL ->]. move: (slS _ lL) => /Zo_P [/setXb_P[_ _ hb] _]; apply: hb; ue. have Ha i: nonempty (range (Lg L (Vg^~ i))) by apply:nonempty_range. have xs: inc x prl_ne2_sigma. rewrite /x;apply/Zo_P; split. apply/setXb_P; split; aw; fprops; rewrite FS_domain => i iI; rewrite LgV//. rewrite setIf_alt; apply: (FS_inter iI (Hb _ iI) (Ha i)). split. move => i iI; rewrite LgV//. rewrite setIf_alt; apply: ((H _ iI) _ (Hb _ iI) (Ha i)). move/Lg_range_P => [t ta ee]. move: (slS _ ta) => /Zo_P [/setXb_P[_ _ hb] [qa _]]. by move: (qa _ iI); rewrite - ee => /nonemptyP. move => a b /Lg_range_P [u ua ub] /Lg_range_P [v va vb]. rewrite ub vb. move: prl_ne2_sigma_osr => [qa qb]. have qc:sub L (substrate prl_ne2_sigma_order) by rewrite qb. move: (proj2 toL u v); rewrite (iorder_sr qa qc) => qd. case: (qd ua va) => /iorder_gle1 /graph_on_P1 [_ _ h]; move: (h _ iI) => k. by exists (Vg v i); split => //; apply/Lg_range_P;exists v. by exists (Vg u i); split => //; apply/Lg_range_P;exists u. move => i j lij. move: (arg1_sr lij) (arg2_sr lij); rewrite ps_substrate_r => iI jI. case:(ps_function_f lij); aw => [ff sf tf]. have ha:sub (intersectionf L (Vg^~ j)) (source (Vg (psf S) (J i j))). rewrite sf => t/(setIf_P _ Lne) w. move: Lne => [l lL]; move: (w l lL);aw. have /(Hb _ jI) hd: inc (Vg l j) (range (Lg L (Vg^~ j))). apply/Lg_range_P; ex_tac. move:((FS_range jI) _ hd) => /setP_P; apply. move => t /(Vf_image_P ff); rewrite LgV// => hc; move: (hc ha)=> [u ui ->] {hc}. rewrite LgV//; apply/(setIf_P _ Lne) => l lL. move/(setIf_P _ Lne): ui => h; move: (h _ lL) => up {h}. move:(slS _ lL) => /Zo_P [qa [_ qb]]; apply: (qb _ _ lij). apply/(Vf_image_P ff); last by ex_tac. move/setXb_P:qa => [_ _]; rewrite FS_domain sf=> h; move: (h _ jI) => hc. by move /setP_P:(FS_range jI hc). exists x; split; first by rewrite sr. move => y yL; apply/graph_on_P1;split => //; first by apply:slS. by move => i iI; rewrite /x LgV// => t /(setIf_P _ Lne); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)