proposition: Lemma prl_rest_can_cofinal_bf S J (H: sub J (psI S)): cofinal (psr S) J -> right_directed_on (psr S) J -> bijection (prl_restr_canonical H).
proof: Proof. move => pa pb. move:(prl_restr_canonical_fp H) => [fg sg tg]. have ax:= (prl_restr_canonical_ax H). move:(proj2 pa);rewrite ps_substrate_r => cof. split. split => //; rewrite sg => x y xp yp. rewrite /prl_restr_canonical; aw => sr. move:(xp)(yp)=>/prl_limitP [xg dx xv xw]/prl_limitP[ yg dy yv yw]. apply: fgraph_exten => //; rewrite dx // => i iI. move:(cof _ iI) =>[j jJ lij]. rewrite (xw _ _ lij) (yw _ _ lij); congr Vf. move:(f_equal (Vg^~j) sr); rewrite !LfV // !LgV//. split => //; rewrite sg tg => y. move: (prl_restr_prop H) => [pE pI pr pf]. move/prl_limitP =>[]; rewrite pE pr pf => yg yd yv yw. have yi0 k: inc k J -> inc (Vg y k) (Vg (psE S) k). by move: yv; aw => yv kJ; move: (yv _ kJ); rewrite LgV. pose idx i := choose (fun j => inc j J /\ gle (psr S) i j). have idx1p i: inc i (psI S) -> inc (idx i) J /\ gle (psr S) i (idx i). move/cof => [j ja jb]. apply: (choose_pr (p:= (fun j => inc j J /\ gle (psr S) i j))); by exists j. pose xi i := Vf (Vg (psf S) (Pair.J i (idx i))) (Vg y (idx i)). have idx2 i j: inc j J -> gle (psr S) i j -> xi i = Vf (Vg (psf S) (Pair.J i j)) (Vg y j). move => jJ le1. move: (prl_prop0 le1) => [iI _]. move:(idx1p _ iI) => [ixJ le2]. move:(pb _ _ jJ ixJ) => [k [kJ le11 le22]]. have le1': gle (induced_order (psr S) J) j k by apply/iorder_gleP. have le2': gle (induced_order (psr S) J) (idx i) k by apply/iorder_gleP. rewrite /xi (yw _ _ le1') (yw _ _ le2') !LgV//. have yi: inc (Vg y k) (Vg (psE S) k) by apply: yi0. by rewrite (prl_prop3 le2 le22 yi) (prl_prop3 le1 le11 yi). set x := Lg (psI S) xi. have xp1: inc x (productb (psE S)). rewrite /x;apply/setXb_P;split; rewrite ? ps_domain_E; aww. move => i iI. move: (idx1p _ iI) => [sa sb]. move:(ps_function_f sb); aw => -[fij sij tij]. by rewrite LgV ///xi - tij; Wtac; rewrite sij; apply: yi0. have xp: inc x (projective_limit S). apply/Zo_P; split => // i j lij. have [iI jI] := (prl_prop0 lij). move:(cof _ jI) => [k kJ ljk]. have lik:= (proj33 (ps_preorder_r S) _ _ _ lij ljk). rewrite /x !LgV//; rewrite (idx2 _ _ kJ ljk) (idx2 _ _ kJ lik). exact (sym_eq (prl_prop3 lij ljk (yi0 _ kJ))). have dy': J = domain y by rewrite yd; aw. exists x => //; rewrite /prl_restr_canonical LfV//. symmetry;apply: fgraph_exten => //; aww => j jJ; rewrite LgV //. move:(H _ jJ) => jI. have lejj:=(prl_prop1 jI). rewrite /x LgV// (idx2 j j jJ lejj) (prl_prop5 jI) //. by move: (yv _ jJ); rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)