proposition: Lemma adjunction_closed : rel_adjunction -> closed e' [preim h of a].
proof: Proof. case=> _ Ae'e; apply: intro_closed => // x' y' /connect1 e'xy a_x. by rewrite Ae'e // in e'xy; rewrite !inE -(ccl_a e'xy). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)