proposition: Lemma prl_prop2 S i j k: gle (psr S) i j -> gle (psr S) j k -> Vg (psf S) (J i j) \coP Vg (psf S) (J j k).
proof: Proof. rewrite /composable. by move => /ps_function_f [fa -> _] /ps_function_f [fb _ ->]; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)