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