proposition: Lemma eq_cln_iso (v v' : G) : N[v] = N[v'] -> induced [set~ v'] ≃ induced [set~ v].
proof: Proof. have [-> _|vDv' Nvv'] := eqVneq v v'; first exact: diso_id. have vv' : v -- v'. by move/setP/(_ v') : Nvv'; rewrite v_in_clneigh in_cln /dominates (negbTE vDv'). set Hv := induced [set~ v']; set Hv' := induced _. have [vI v'I] : v \in [set~ v'] /\ v' \in [set~ v] by rewrite !inE [v' == _]eq_sym (sg_edgeNeq vv'). pose f (x : Hv) : Hv' := insubd (Sub v' v'I) (val x). pose g (x : Hv') : Hv := insubd (Sub v vI) (val x). have can_f : cancel f g. { move => x. apply: val_inj. rewrite /f/g/= !val_insubd !inE !SubK. have [/= ->|/=] := eqVneq (val x) v; rewrite ?eqxx // ifT // -in_set1 -in_setC. exact (valP x). } have can_g : cancel g f. { move => x. apply: val_inj. rewrite /f/g/= !val_insubd !inE !SubK. have [/= ->|/=] := eqVneq (val x) v'; rewrite ?eqxx // ifT // -in_set1 -in_setC. exact (valP x). } apply: Diso' can_f can_g _. move => [x px] [y py]; rewrite /f/=. rewrite /edge_rel/= !val_insubd !SubK !inE. rewrite !inE in px py. have [?/=|/=] := eqVneq x v; subst. have [->|/= yDv] := eqVneq y v; [by rewrite !sgP | by rewrite (cln_eq Nvv')]. by have [->/= xDv|//] := eqVneq y v; rewrite [RHS]sgP (cln_eq Nvv') // sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)