proposition: Lemma dst_not_reachable: forall x pa y, vvalid g x -> dst g (out_edge x) = pa -> reachable g pa y -> ~ reachable g y x.
proof: Proof. intros. intro. assert (g |= (x, (out_edge x) :: nil) is x ~o~> pa satisfying (fun _ => True)). { split; split; auto. - simpl. unfold strong_evalid. rewrite H0. pose proof (vvalid_src_evalid x H). destruct H3. rewrite H3. split; [|split; [|split]]; auto. apply reachable_head_valid in H1. auto. - red. rewrite Forall_forall. split; intros; auto. } assert (reachable g pa x) by (apply reachable_trans with y; auto). destruct H4 as [ppa ?]. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H3 H4). apply no_loop_path in H5. unfold path_glue in H5. simpl in H5. inversion H5. 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