proposition: Lemma prl_map2_compose S S' S'' u v (F := projective_limit_fun) (w:= Lg (psI S) (fun i => (Vg v i) \co (Vg u i))) : prl_same_index S S' -> prl_same_index S' S'' -> prl_map2_compat S S' u -> prl_map2_compat S' S'' v -> prl_map2_compat S S'' w /\ F S S'' w = F S' S'' v \co F S S' u.
proof: Proof. move => sb1 sb2 hu hv. have sb3: prl_same_index S S'' by rewrite /prl_same_index sb1. move:(prl_map2_prop sb1 hu); rewrite -/F => pa1. move:(prl_map2_prop sb2 hv); rewrite -/F => pa2. move: hu hv=> [cpa1 cpa2 cpa3 cpa4] [cpb1 cpb2 cpb3 cpb4]. have ssI:= prl_same_index_same_I sb1. rewrite - ssI in cpb3. have ha i: inc i (psI S) -> Vg v i \coP Vg u i. move => iI. move: (cpa3 _ iI) (cpb3 _ iI) =>[fu su tu] [fv sv tv]. by split => //;rewrite sv tu. have hb i j: gle (psr S) i j -> Vg u i \coP Vg (psf S) (J i j). move => lij. move:(ps_function_f lij)(prl_prop0 lij) => [ff sf tf] [ /cpa3 [fu su tu] _]. by split => //; rewrite su tf; aw. have hb' i j: gle (psr S') i j -> Vg v i \coP Vg (psf S') (J i j). move => lij; move:(lij); rewrite - sb1 => lij'. move:(ps_function_f lij) (prl_prop0 lij')=> [ff sf tf] [ /cpb3 [fu su tu] _]. by split => //; rewrite su tf; aw. have hc i j: gle (psr S) i j -> Vg (psf S') (J i j) \coP Vg u j. move => lij; move:(lij); rewrite sb1 => lij'. move:(ps_function_f lij') (prl_prop0 lij) => [ff sf tf] [_ /cpa3 [fu su tu]]. by split => //; rewrite sf tu; aw. have hc' i j: gle (psr S) i j -> Vg (psf S'') (J i j) \coP Vg v j. move => lij; move:(lij); rewrite sb1 sb2 => lij'. move: (prl_prop0 lij) (ps_function_f lij') => [_ /cpb3[fu su tu]] [ff sf tf]. by split => //; rewrite sf tu; aw. have cpc:prl_map2_compat S S'' w. rewrite /w; split; aww. move => i iI; rewrite LgV//. move:(cpa3 _ iI) (cpb3 _ iI) => [fu su tu] [fv sv tv]. by saw;fct_tac; rewrite sv tu. move => i j lij. have lij': gle (psr S') i j by rewrite - sb1. move:(prl_prop0 lij)=> [isr jsr]; rewrite !LgV//. rewrite - (compfA (ha _ isr) (hb _ _ lij)) (cpa4 _ _ lij). rewrite (compfA (hb' _ _ lij') (hc _ _ lij)) (cpb4 _ _ lij'). by rewrite (compfA (hc' _ _ lij) (ha _ jsr)). split; first exact. apply:(prl_map2_unique sb3 cpc (prl_map2_prop sb3 cpc)). move: pa1 pa2=> [[ff sf tf] ra2] [ [ff' sf' tf'] ra4]. have ra3: F S' S'' v \coP F S S' u by split => //; rewrite sf' tf. split; first by saw; apply: compf_f. move => i iI. have ssI':= prl_same_index_same_I sb3. have iI': inc i (psI S') by rewrite - ssI. have iI'': inc i (psI S'') by rewrite - ssI'. move: (prl_can_fun_fp iI'') => [fpl'' spl'' tpl'']. move: (prl_can_fun_fp iI') => [fpl' spl' tpl']. move: (prl_can_fun_fp iI) => [fpl spl tpl]. move: (cpb3 _ iI) => [fv sv tv]. move: (cpa3 _ iI) => [fu su tu]. have qa: prl_can_fun S'' i \coP F S' S'' v. by split => //; rewrite spl'' tf'. have qb: Vg v i \coP prl_can_fun S' i by split => //; rewrite sv tpl'. have qc: prl_can_fun S' i \coP F S S' u. by split => //; rewrite spl' tf. have qd: Vg u i \coP prl_can_fun S i by split => //; rewrite su tpl. rewrite (compfA qa ra3) - (ra4 _ iI') - (compfA qb qc) - (ra2 _ iI). rewrite (compfA (ha _ iI) qd) /w LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)