proposition: Lemma strict_adjunction : injective h -> a \subset codom h -> rel_base h e e' [predC a] -> rel_adjunction.
proof: Proof. move=> /= injh h_a a_ee'; pose h' x Hx := iinv (subsetP h_a x Hx). apply: (@intro_adjunction h') => [x a_x | x' a_x]. rewrite f_iinv connect0; split=> // y a_y e_xy. by rewrite connect1 // -a_ee' !f_iinv ?negbK. rewrite [h' _ _]iinv_f //; split=> // y' e'xy. by rewrite connect1 // a_ee' ?negbK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)