proposition: Lemma ex9_map_aux x y: related ex9_rels_ext x y -> Vf (Vg u (Q x)) (P x) = Vf (Vg u (Q y)) (P y).
proof: Proof. have Ha a b: inc a ex9_G -> inc b ex9_G -> ex9_rel a b -> Vf (Vg u (Q a)) (P a) = Vf (Vg u (Q b)) (P b). move => /ex9G_P [pa aI aE] /ex9G_P [pb bI bE] [leij ->]. case:(function_f leij); aw => fij sij tij. move:(function_u bI) => [fu su tu]. have ax1: Vg u (Q b) \coP Vg f (J (Q a) (Q b)) by split => //; ue. have pas: inc (P a) (source (Vg f (J (Q a) (Q b)))) by ue. rewrite - (compose_u leij) compfV//. have H a b: ex9_rels a b -> Vf (Vg u (Q a)) (P a) = Vf (Vg u (Q b)) (P b). move => [aG bG]; case => h1;[ by apply Ha | by symmetry; apply: Ha]. move/graph_on_P1 => [ _ _ [c [cc <- <-]]] {x y}. elim:c cc; first by move => x y /=; apply: H. by move => x c Hr /= [qa qb]; rewrite (H _ _ qa); apply: Hr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)