proposition: Lemma prl_r3_F_can_bf: bijection prl_r3_F_can.
proof: Proof. rewrite /prl_r3_F_can;apply:lf_bijective; first by apply: prl_r3_F_can_ax. move => u v upl vpl sr. move/prl_limitP:upl => [fgu du uv uw]. move/prl_limitP:vpl => [fgv dv vv vw]. have sdu: domain u = domain v by rewrite du dv. apply:(fgraph_exten fgu fgv sdu); rewrite du => j jI. move:(prl_r3_qprop0 jI)(set1_1 j) => sL jsj. move: (f_equal (fun z => Vg (Vg z (singleton j)) j) sr). rewrite /prl_r3_restr_fun !LgV//. move => y yp. move:prl_r3_F_prop => [E_F I_F r_F f_F]. have da: domain (psE prl_r3_F) = prl_r3_nI by rewrite E_F; aw. move/Zo_P:(yp) => [/setXb_P [fgy dy yv] yw]. rewrite da in dy yv; rewrite r_F in yw; rewrite E_F in yv. have yab a b: gle prl_r3_nr a b -> Vg y a = restr (Vg y b) a. move => lab;move: (yw _ _ lab); rewrite f_F LgV//. move:(prl_r3_prop7 lab) => ax1. move/(sub_gleP):lab => [_ bsr _]. by rewrite/prl_r3_gij LfV//; aw; move: (yv b bsr);rewrite LgV //. pose xi i := Vg (Vg y (singleton i)) i. have idx2 i j: inc j prl_r3_nI -> inc i (psI S)-> inc i j -> xi i = Vg (Vg y j) i. move => jL iI ij. have siL:= prl_r3_qprop0 iI. have kL:= (prl_r3_nI_stable_union jL siL). have j1k: gle prl_r3_nr j (j +s1 i) by apply/sub_gleP; split; fprops. have j2k: gle prl_r3_nr (singleton i) (j +s1 i). by apply/sub_gleP; split; fprops=> t /set1_P ->; fprops. move:(prl_r3_prop7 j1k) (prl_r3_prop7 j2k) (yv _ kL). rewrite LgV// => ax1 ax2 ii. rewrite /xi (yw _ _ j1k) (yw _ _ j2k) f_F /prl_r3_gij !LgV//; aw. rewrite ! LfV// ! LgV//; fprops. set x := Lg (psI S) xi. have xx i (iL: inc i prl_r3_nI): inc (Vg y i) (projective_limit (prl_restr (prl_r3_prop4 iL))). move: (yv _ iL); rewrite LgV ///prl_r3_Fl /prl_r3_systemi. by case: (ixm (inc i prl_r3_nI)). have xpe: inc x (productb (psE S)). apply/setXb_P; rewrite /x ps_domain_E ; split; aww. move => i iI; rewrite LgV//; have sa := (prl_r3_qprop0 iI). move/Zo_P:(xx _ sa). move: (prl_restr_prop (prl_r3_prop4 sa)) =>[ka kb kc kd]; rewrite ka kc kd. move => [] /setXb_P [fgu]; aw; move => du uv _. move: (uv _ (set1_1 i)); rewrite LgV; fprops. have yve: y = prl_r3_restr_fun x. move/setXb_P: xpe =>[xa xb xc]. rewrite /prl_r3_restr_fun;apply: fgraph_exten; aww. rewrite dy => i iL;move: (xx _ iL);move /Zo_P. move: (prl_restr_prop (prl_r3_prop4 iL)) =>[ka kb kc kd]; rewrite ka kc kd. move => [] /setXb_P [fgu]; aw; move => dyi yip1 yip2; rewrite LgV//. apply: fgraph_exten => //; aww. rewrite dyi /x => j di;move/Zo_P:(iL) => [/setP_P h _]; move: (h _ di) => jI. by rewrite !LgV // (idx2 _ _ iL jI di). exists x => //; apply/Zo_P; split => //. move => i j lij. move:(arg1_sr lij) (arg2_sr lij);rewrite ps_substrate_r => iI jI. move: (prl_r3_qprop1 lij) => [J [jL iJ jJ]]. rewrite/x (LgV iI) (LgV jI) (idx2 _ _ jL iI iJ) (idx2 _ _ jL jI jJ). have ll: gle(induced_order (psr S) J) i j by apply/iorder_gleP. move: (xx _ jL) => /Zo_P [yp1 yp2]. by rewrite (yp2 _ _ ll)/prl_restr /= LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)