proposition: Lemma adjacent_reachable: forall g u v, adjacent g u v -> (reachable g u v \/ reachable g v u).
proof: Proof. intros. unfold adjacent, adj_edge in H. destruct H as [e [? [[? ?] | [? ?]]]]; [left | right]; unfold reachable, reachable_by, reachable_by_path. - exists (u, (e::nil)); split. + split; trivial. + unfold good_path. split; simpl. * split; trivial; symmetry; trivial. * unfold path_prop. split; trivial. rewrite Forall_forall; intros; split; trivial. - exists (v, e::nil); split. + split; trivial. + unfold good_path. split; simpl. * split; trivial; symmetry; trivial. * unfold path_prop. split; trivial. rewrite Forall_forall; intros; split; trivial. 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