proposition: Lemma reachable_implies_connected: forall g u v, reachable g u v -> connected g u v.
proof: Proof. intros. unfold reachable_by in H. destruct H. destruct H. rename x into dp. exists (epath_to_vpath g dp). split. apply valid_dpath_implies_valid_upath. apply H0. destruct H0. clear H1. destruct dp; destruct l. unfold path_ends in H; unfold phead in H; destruct H. split; simpl. rewrite H; reflexivity. unfold pfoot in H1. unfold pfoot' in H1. rewrite H1; reflexivity. unfold path_ends in H. destruct H. unfold phead in H. split. rewrite H. apply epath_to_vpath_head. rewrite <- H. apply H0. rewrite epath_to_vpath_foot. rewrite H1. reflexivity. apply H0. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph