proposition: Lemma Exercise7_2 S: right_directed (psr S) -> (forall i j, gle (psr S) i j -> injection (Vg (psf S) (J i j))) -> forall i, inc i (psI S) -> injection (prl_can_fun S i).
proof: Proof. move => ha hb i iI. have exi:=(prl_proj_ax iI). move:(prl_can_fun_fp iI) => [ffi sfi tfi]. split => //; rewrite sfi => x y xpl ypl. rewrite /prl_can_fun; rewrite !LfV// => svi. move/prl_limitP: xpl => [fgx dx xv xw]. move/prl_limitP: ypl => [fgy dy yv yw]. apply: fgraph_exten => //; first by rewrite dx dy. rewrite dx => j jde. have isr: inc i (substrate (psr S)) by rewrite ps_substrate_r. have jsr: inc j (substrate (psr S)) by rewrite ps_substrate_r. move/right_directedP: ha => [_ h]; move:(h _ _ isr jsr)=> [k [ka kb]] {h}. move: svi. rewrite (xw _ _ ka) (yw _ _ ka) (xw _ _ kb) (yw _ _ kb) => svk. move:(ps_function_f ka) => [fik sik tik]. have kk: inc k (psI S) by move:(arg2_sr ka); rewrite ps_substrate_r. have xs1: inc (Vg x k) (source (Vg (psf S) (J i k))). by rewrite sik pr2_pair; apply: xv. have ys1: inc (Vg y k) (source (Vg (psf S) (J i k))). by rewrite sik pr2_pair; apply: yv. by rewrite (proj2 (hb _ _ ka) _ _ xs1 ys1 svk). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)