proposition: Lemma epath_to_vpath_path_glue_one_step: forall (g: AdjMatGG) (a b c : V) p, valid_path g p -> path_ends g p a b -> Permutation (epath_to_vpath g (path_glue p (b, (b, c)::nil))) (c :: epath_to_vpath g p).
proof: Proof. intros. rewrite (surjective_pairing p) in *. remember (snd p) as a2b. replace (fst p) with a in *. 2: destruct H0 as [? _]; simpl in H0; Lia.lia. clear Heqa2b. generalize dependent H. generalize dependent H0. generalize dependent b. generalize dependent a. generalize dependent a2b. induction a2b. - intros. simpl. red in H0. simpl in H0; destruct H0 as [_ ?]. subst a. rewrite (edge_dst_snd g), (edge_src_fst g); simpl. apply perm_swap. - intros. rename a into new. inversion H. clear H2. unfold path_glue. simpl fst; simpl snd. rewrite <- app_comm_cons. repeat rewrite epath_to_vpath_cons_eq; trivial. pose proof (perm_swap c a0 (epath_to_vpath g (dst g new, a2b))). apply Permutation_trans with (l' := (a0 :: c :: epath_to_vpath g (dst g new, a2b))); trivial. apply perm_skip. apply IHa2b. + red. split; trivial. destruct H0. rewrite pfoot_cons in H3; trivial. + apply valid_path_cons in H; 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