proposition: Lemma ex1_F_can_bf: bijection ex1_F_can.
proof: Proof. rewrite /ex1_F_can;apply:lf_bijective; first by apply: ex1_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 - ex1_prop3 - HJI. move => j /setUb_P [k kdj jv]; rewrite HJd in kdj. move: (f_equal (Vg ^~k) sr); rewrite/ex1_restr_fun LgV// => sr'. by move: (f_equal (Vg ^~j) sr'); rewrite !LgV//. move => y yp. have HL3 i j: inc i L -> inc j L -> exists k, [/\ inc k L, gle rL i k & gle rL j k]. move => iL jL. have isr: inc i (substrate rL) by rewrite HLs. have jsr: inc j (substrate rL) by rewrite HLs. move:(HLd isr jsr) => [k [i1k i2k]]. move:(arg2_sr i1k); rewrite HLs => kL; by exists k. move:ex1_F_prop => [E_F I_F r_F f_F]. have da: domain (psE ex1_F) = L 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. have yab a b: gle rL a b -> Vg y a = restr (Vg y b) (Vg Jf a). move => lab;move: (yw _ _ lab); rewrite f_F LgV//. have bsr:= (proj2 (ex1_prop2 lab)). move:(ex1_prop7 lab) => ax1. rewrite/ex1_gij; aw; rewrite LfV//. move: (yv b bsr); rewrite E_F LgV//. have ha i j1 j2: inc j1 L -> inc j2 L -> inc i (Vg Jf j1) -> inc i (Vg Jf j2) -> Vg (Vg y j1) i = Vg (Vg y j2) i. move => j1l j2l ij1 ij2. move:(HL3 _ _ j1l j2l) => [k [kL j1k j2k]]. by rewrite (yab _ _ j1k) (yab _ _ j2k) ! LgV//. pose idx i := choose (fun j => inc j L /\ inc i (Vg Jf j)). have idx1p i: inc i I -> inc (idx i) L /\ inc i (Vg Jf (idx i)). rewrite - HJI => /setUb_P [k ka kb]. apply: (choose_pr (p:= (fun j => inc j L /\ inc i (Vg Jf j)))). by rewrite - HJd; exists k. pose xi i := Vg (Vg y (idx i)) i. have idx2 i j: inc j L -> inc i (Vg Jf j) -> xi i = Vg (Vg y j) i. move => jL ij; move: (idx1p _ (ex1_prop1 jL ij)) => [hu hv]. by apply:ha. set x := Lg I xi. have xx i (iL: inc i L): inc (Vg y i) (projective_limit (prl_restr (ex1_prop4 iL))). move: (yv _ iL); rewrite E_F LgV// /ex1_Fl /ex1_systemi. by case: (ixm (inc i L)). have xpe: inc x (productb (psE S)). apply/setXb_P; rewrite /x ps_domain_E - ex1_prop3; split; aww. move => i iI; rewrite LgV//. move:(idx1p _ iI) => [sa sb]. move: (xx _ sa); move /Zo_P. move: (prl_restr_prop (ex1_prop4 sa)) =>[ka kb kc kd]; rewrite ka kc kd. move => [] /setXb_P [fgu]; aw; move => du uv _. by move: (uv _ sb); rewrite LgV. have yve: y = ex1_restr_fun x. move/setXb_P: xpe =>[xa xb xc]. rewrite /ex1_restr_fun;apply: fgraph_exten; aww. rewrite dy => i iL;move: (xx _ iL);move /Zo_P. move: (prl_restr_prop (ex1_prop4 iL)) =>[ka kb kc kd]; rewrite ka kc kd. move => [] /setXb_P [fgu]; rewrite LgV//;aw; move => dyi yip1 yip2. apply: fgraph_exten => //; aww. rewrite dyi /x => j di; have jI:=(ex1_prop1 iL di). by rewrite ! LgV //(idx2 _ _ iL di). exists x => //; apply/Zo_P; split => //. move => i j lij. move:(arg1_sr lij) (arg2_sr lij); rewrite rS HIs => iI jI. move:(idx1p _ iI) (idx1p _ jI) => [pa pb][pc pd]. rewrite /x /xi; rewrite !LgV //. move:(HL3 _ _ pa pc) => [k [kL j1k j2k]]. have ii: inc i (Vg Jf k) by apply: (HJm j1k). have jj: inc j (Vg Jf k) by apply: (HJm j2k). rewrite (ha i (idx i) k pa kL pb ii). rewrite (ha j (idx j) k pc kL pd jj). have ll: gle(induced_order (psr S) (Vg Jf k)) i j by apply/iorder_gleP. move: (xx _ kL) => /Zo_P [yp1 yp2]. rewrite (yp2 _ _ ll)/prl_restr /= LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)