proposition: Lemma adjunction_n_comp : rel_adjunction -> n_comp e a = n_comp e' [preim h of a].
proof: Proof. case=> Aee' Ae'e. have inj_h: {in predI (roots e') [preim h of a] &, injective (root e \o h)}. move=> x' y' /andP[/eqP r_x' /= a_x'] /andP[/eqP r_y' _] /(rootP sym_e). by rewrite -Ae'e // => /(rootP sym_e'); rewrite r_x' r_y'. rewrite /n_comp_mem -(card_in_image inj_h); apply: eq_card => x. apply/andP/imageP=> [[/eqP rx a_x] | [x' /andP[/eqP r_x' a_x'] ->]]; last first. by rewrite /= -(ccl_a (connect_root _ _)) roots_root. have [y' e_xy]:= Aee' x a_x; pose x' := root e' y'. have ay': h y' \in a by rewrite -(ccl_a e_xy). have e_yx: connect e (h y') (h x') by rewrite -Ae'e ?connect_root. exists x'; first by rewrite inE /= -(ccl_a e_yx) ?roots_root. by rewrite /= -(rootP sym_e e_yx) -(rootP sym_e e_xy). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)