proposition: Lemma iso_connected (G H : sgraph) : diso G H -> connected [set: H] -> connected [set: G].
proof: Proof. move=> [[h g can_h can_g] /= hom_h hom_g] con_H x y _ _. rewrite restrictE; last by move => z; rewrite !inE. have := con_H (h x) (h y). rewrite !inE => /(_ isT isT). rewrite restrictE; last by move => z; rewrite !inE. case/pathpP => p. case/lift_pathp => //. + move => {x y} x y. rewrite -{2}[x]can_h -{2}[y]can_h. exact: hom_g. + exact: can_inj can_h. + move => z _. apply/codomP. exists (g z). by rewrite can_g. + move => p' [Hp' _]. apply/pathpP. by exists p'. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)