proposition: Lemma ex5_Gij_prop2 i j y: gle (psr S) i j -> inc y (Vg Gf i) -> exists2 x, inc x (Vg Gf j) & y = Vf (ex5_f i j) x.
proof: Proof. move => lij; rewrite -(ex5_G6 lij) => yj. move:(prl_prop4 lij) => [fij sij tij]. move:(ex5_G4 (proj2 (prl_prop0 lij))); rewrite - sij => ss. by move/(Vf_image_P fij ss): yj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)