proposition: Lemma toEdgeList_tail: forall len x r, exists l, toEdgeList (len, x, r) = l ++ r.
proof: Proof. intros. remember (lengthInput (len, x, r)). assert (lengthInput (len, x, r) <= n) by lia. clear Heqn. revert len x r H. induction n; intros; simpl. + unfold lengthInput in H. rewrite toEdgeList_unfold. destruct (Compare_dec.le_dec len (length r)). exists nil; simpl; auto. exfalso; lia. + unfold lengthInput in H. rewrite toEdgeList_unfold. destruct (Compare_dec.le_dec len (length r)). exists nil; simpl; auto. simpl. destruct (filterE (edge_func g x)). exists nil; simpl; auto. assert (lengthInput (len, dst g e, (e, dst g e) :: r) <= n) by (simpl; lia). apply IHn in H0. destruct H0 as [l' ?]. exists (l' ++ (e, dst g e) :: nil). rewrite <- app_assoc, <- app_comm_cons. simpl. 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.FiniteGraph