proposition: Lemma prl_ne2_res4b i: inc i (psI S) -> prl_ne1_condii' i -> nonempty (prl_ne2_res_RHS i).
proof: Proof. move => iI ha. rewrite /prl_ne2_res_RHS setIf_alt. have hd: forall j, gle (psr S) i j -> nonempty (Imf (Vg (psf S) (J i j))). move => j leij. move:(prl_prop0 leij) =>[_ jI]. move: (prl_prop4 leij) => [ff sf tf]. move: (prl_ne2_ne jI) => [x xe]. exists (Vf (Vg (psf S) (J i j)) x); apply/(Imf_P ff). rewrite sf; ex_tac. have sub_rec j k: gle (psr S) i j -> gle (psr S) j k -> sub (Imf (Vg (psf S) (J i k))) (Imf (Vg (psf S) (J i j))). move => lij ljk. move: (proj33 (ps_preorder_r S)_ _ _ lij ljk) => lik. move:(prl_prop4 lik) => [fik sik tik]. move:(prl_prop4 ljk) => [fjk sjk tjk]. move:(prl_prop4 lij) => [fij sij tij]. move => t /(Imf_P fik); rewrite sik; move => [u ue ->]. apply /(Imf_P fij); rewrite sij -(prl_prop3 lij ljk ue). exists (Vf (Vg (psf S) (J j k)) u) => //; Wtac. apply: ha. - move => t /Lg_range_P [j /Zo_P[jI lij] ->]; apply:(FS_prop_iv lij). by move:(prl_prop4 lij) => [ff -> tf]; apply: FS_whole. - exists (Vg (psE S) i); apply/Lg_range_P; exists i. apply:(prl_ne2_int_i iI). by rewrite prl_ne2_im_of_id. - move => /Lg_range_P [ j /Zo_P[jI lij]] => be. by move:(hd _ lij); rewrite - be => /nonemptyP. - move => x y /Lg_range_P [j1 /Zo_P[j1I leij1] ->]. move => /Lg_range_P [j2 /Zo_P[j2I leij2] ->]. move:(rdr (arg2_sr leij1) (arg2_sr leij2)) =>[k [lej1k lej2k]]. exists (Imf (Vg (psf S) (J i k))); split. apply/Lg_range_P; exists k => //. apply/prl_ne2_intP=> //; exact:(proj33 (ps_preorder_r S)_ _ _ leij1 lej1k). by apply: sub_rec. by apply: sub_rec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)