proposition: Lemma prl_dl3_ffam_comp i j k: gle r i j -> gle r j k -> Vg prl_dl3_ffam (J i j) \co Vg prl_dl3_ffam (J j k) = Vg prl_dl3_ffam (J i k).
proof: Proof. move => lij ljk; move:(proj33 or _ _ _ lij ljk) => lik. rewrite /prl_dl3_ffam !LgV//. have hc l: inc l L -> graph (Vg (psf (fS l)) (J i j)) \cfP graph (Vg (psf (fS l)) (J j k)). move => lL. have ha: gle (psr (fS l)) i j by rewrite fSr. have hb: gle (psr (fS l)) j k by rewrite fSr. move:(ps_function_f ha) (ps_function_f hb) => [ff sf _] [ff' _ tf]. rewrite pr2_pair in sf; rewrite pr1_pair in tf. split; fprops. rewrite domain_fg // sf - tf. exact: (proj33 (corr_propc (proj31 ff'))). aw; apply:ext_map_prod_compose. - by move: (prl_dl3_ffam_ax ljk); aw. - by move: (prl_dl3_ffam_ax lij); aw. - move => l lL. have ha: gle (psr (fS l)) i j by rewrite fSr. have hb: gle (psr (fS l)) j k by rewrite fSr. rewrite -(ps_compose_f ha hb) /compose; aw; symmetry;apply:compg_composef. by apply: hc. - apply: hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)