proposition: Lemma prl_prop3 S y i j k (f:= psf S): gle (psr S) i j -> gle (psr S) j k -> inc y (Vg (psE S) k) -> Vf (Vg f (J i j)) (Vf (Vg f (J j k)) y) = Vf (Vg f (J i k)) y.
proof: Proof. move => lij ljk yv. have co:= (prl_prop2 lij ljk). move:(f_equal (Vf^~ y) (ps_compose_f lij ljk)); rewrite !compfV//. by move:(ps_function_f ljk) => [_ -> _]; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)