proposition: Lemma intro_adjunction (h' : forall x, x \in a -> T') : (forall x a_x, [/\ connect e x (h (h' x a_x)) & forall y a_y, e x y -> connect e' (h' x a_x) (h' y a_y)]) -> (forall x' a_x, [/\ connect e' x' (h' (h x') a_x) & forall y', e' x' y' -> connect e (h x') (h y')]) -> rel_adjunction.
proof: Proof. move=> Aee' Ae'e; split=> [y a_y | x' z' a_x]. by exists (h' y a_y); case/Aee': (a_y). apply/idP/idP=> [/connectP[p e'p ->{z'}] | /connectP[p e_p p_z']]. elim: p x' a_x e'p => //= y' p IHp x' a_x. case: (Ae'e x' a_x) => _ Ae'x /andP[/Ae'x e_xy /IHp e_yz] {Ae'x}. by apply: connect_trans (e_yz _); rewrite // -(closed_connect cl_a e_xy). case: (Ae'e x' a_x) => /connect_trans-> //. elim: p {x'}(h x') p_z' a_x e_p => /= [|y p IHp] x p_z' a_x. by rewrite -p_z' in a_x *; case: (Ae'e _ a_x); rewrite sym_e'. case/andP=> e_xy /(IHp _ p_z') e'yz; have a_y: y \in a by rewrite -(cl_a e_xy). by apply: connect_trans (e'yz a_y); case: (Aee' _ a_x) => _ ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)