proposition: Lemma cln_eq (x x' y : G) : N[x] = N[x'] -> y != x -> y != x' -> x -- y = x' -- y.
proof: Proof. by move/setP=> /(_ y); rewrite !inE; case: (eqVneq x y); case: (eqVneq x' y). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)