proposition: Lemma in_eq_n_comp e e' a : connect_sym e -> connect_sym e' -> closed e a -> closed e' a -> {in a &, e =2 e'} -> n_comp e a = n_comp e' a.
proof: Proof. move => sym_e sym_e' cl_e cl_e' eq_e. have adj_e : rel_adjunction id e e' a. { apply: strict_adjunction => //=. apply/subsetP => z _; exact: codom_id. move => u v u_a. rewrite inE negbK /= in u_a. apply/idP/idP => uv; first by rewrite -eq_e // -(cl_e u v). by rewrite eq_e // -(cl_e' u v). } rewrite [in RHS](eq_n_comp_r (_ : a =i [preim id of a])) //. exact: adjunction_n_comp. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)