proposition: Lemma lst_reachable_or: forall x r1 r2, reachable g x r1 -> reachable g x r2 -> reachable g r1 r2 \/ reachable g r2 r1.
proof: Proof. intros. destruct H as [p1 ?]. destruct H0 as [p2 ?]. destruct (Compare_dec.le_dec (length (snd p1)) (length (snd p2))); [left | right]. - apply (lst_reachable_unique' p1 p2 x); auto. - apply (lst_reachable_unique' p2 p1 x); intuition. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph