Lemma is_connected_pointed (g : graph) (v0 : vertex g) : (∏ (v : vertex g), graph_zig_zag v0 v) -> is_connected g. Proof. intro H. intros v1 v2. use (append_graph_zig_zag (y := v0)). - exact (reverse_graph_zig_zag (H v1)). - exact (H v2). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.