proposition: Lemma in_path_app_cons: forall (g: AdjMatGG) step p2a src a b, valid_path g p2a -> evalid g (a,b) -> path_ends g p2a src a -> In_path g step (fst p2a, snd p2a +:: (a, b)) -> In_path g step p2a \/ step = b.
proof: Proof. intros. destruct H2; simpl in H2. 1: left; unfold In_path; left; trivial. destruct H2 as [? [? ?]]. assert (evalid g x). { apply in_app_or in H2. simpl in H2. destruct H2 as [? | [? | ?]]; [| | Lia.lia]; [|subst;trivial]. rewrite (surjective_pairing p2a) in H. apply (valid_path_evalid _ _ _ _ H H2). } rewrite (edge_src_fst g) in H3; trivial. apply in_app_or in H2; simpl in H2. destruct H2 as [? | [? | ?]]; [| | Lia.lia]; destruct H3. - left. unfold In_path. right. exists x. rewrite (edge_src_fst g); trivial. split; [|left]; trivial. - left. unfold In_path. right. exists x. rewrite (edge_src_fst g); trivial. split; [|right]; trivial. - left. apply pfoot_in. destruct H1. rewrite H3, <- H2; simpl; trivial. - unfold In_path. right. rewrite H3, <- H2; simpl; trivial. rewrite (edge_dst_snd g); trivial. Qed.
imports: Coq.ZArith.BinInt Coq.Classes.EquivDec compcert.lib.Integers CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.FiniteGraph CertiGraph.graph.path_lemmas