proposition: Lemma add_edge_induced_iso (G : sgraph) (S T : {set G}) (u v : induced S) (x y : induced T) : S = T -> val u = val x -> val v = val y -> diso (add_edge (induced S) u v) (add_edge (induced T) x y).
proof: Proof. move=> eq_ST eq_ux eq_vy. have SofT z : z \in T -> z \in S by rewrite eq_ST. have TofS z : z \in S -> z \in T by rewrite eq_ST. set g : induced T -> induced S := fun z => Sub (val z) (SofT (val z) (valP z)). set f : induced S -> induced T := fun z => Sub (val z) (TofS (val z) (valP z)). apply (@Diso'' (add_edge (induced S) _ _) (add_edge (induced T) _ _) f g); rewrite {}/f {}/g. - move => ?. exact: val_inj. - move => ?. exact: val_inj. - move => a b; rewrite /edge_rel /= /edge_rel /=. rewrite -!(inj_eq val_inj) /=. by rewrite eq_ux eq_vy. - move => a b. rewrite /edge_rel /= /edge_rel /=. rewrite -!(inj_eq val_inj) /=. by rewrite eq_ux eq_vy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)