proposition: Lemma prl_can_fun_prop S i j (f := psf S) (fi := prl_can_fun S i) (fj := prl_can_fun S j): gle (psr S) i j -> (Vg f (J i j) \coP fj) /\ fi = (Vg f (J i j)) \co fj.
proof: Proof. move => lij. have [fij sij tij]:=(prl_prop4 lij). have [iE jE]:= (prl_prop0 lij). have [ffi si ti] := (prl_can_fun_fp iE). have [ffj sj tj] := (prl_can_fun_fp jE). have pd: source (Vg f (J i j)) = target fj by rewrite sij. have pe: Vg f (J i j) \coP fj by []. have pf:=(compf_f pe). have pg: source fi = source fj by rewrite si sj. have ph: target fi = target (Vg f (J i j)) by ue. split => //;apply:function_exten => //; aw; trivial => x xsf. rewrite compfV //; last by ue. have xE: inc x (projective_limit S) by rewrite - si. rewrite /fi /fj (prl_proj_ev iE xE) (prl_proj_ev jE xE). by move/Zo_P:xE => [_]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)