proposition: Lemma lst_self_loop: forall x y, dst g (out_edge x) = x -> reachable g x y -> x = y.
proof: Proof. intros. destruct H0 as [[v p] ?]. assert (v = x) by (destruct H0 as [[? _] _]; simpl in H0; auto). subst v. induction p. - destruct H0 as [[_ ?] _]. simpl in H0. auto. - assert (g |= (dst g a, p) is (dst g a) ~o~> y satisfying (fun _ => True)). { clear IHp. destruct H0 as [[? ?] [? ?]]. pose proof H2. apply valid_path_cons in H4. split; split; auto. - rewrite pfoot_cons in H1. auto. - rewrite path_prop_equiv; intros; auto. } assert (dst g a = x). { destruct H0 as [_ [? _]]. simpl in H0. destruct H0. assert (strong_evalid g a) by (destruct p; intuition). clear H2. destruct H3 as [? [? ?]]. rewrite <- H0 in H3. assert (a = out_edge x) by (apply only_one_edge; auto). rewrite <- H5 in H. auto. } apply IHp. rewrite H2 in H1. auto. 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