proposition: Lemma ex9_prope: sub (graph_on ex9_srel ex9_G) ex9_rels_ext.
proof: Proof. move => t /Zo_P [/setX_P[pp Px Qx] [k [leij lejk ff]]]. move:(arg2_sr leij); rewrite sr => kI. move/ex9G_P:(Px) => [ppx Ppx Qpx]. move/ex9G_P:(Qx) => [pqx Pqx Qqx]. rewrite - pp. apply/graph_on_P1; split => //. set z := J (Vf (Vg f (J (Q (P t)) k)) (P (P t))) k. have zg: inc z ex9_G. rewrite /z;apply/ex9G_P; split;aww. case:(function_f leij); aw => fa sa ta; Wtac. exists (chain_next (P t) (chain_pair z (Q t))); split => //=; split. split => //; left; rewrite /z; saw. split => //; right; rewrite /z ff; saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)