proposition: Lemma elabel_Znth_graph_to_mat: forall (g: @EdgeLabGG size) (f: E -> E) src dst out, evalid g (src, dst, out) -> elabel g (f (src, dst, out)) = Znth out (Znth src (graph_to_mat g f)).
proof: Proof. intros. assert (vvalid g src). { apply (evalid_strong_evalid g) in H. destruct H as [_ [? _]]. rewrite edge_src_fst in H; apply H. } rewrite (vvalid_meaning g) in H0. rewrite (evalid_meaning g) in H; destruct H as [_ [ ??]]. assert (0 <= size). { pose proof (size_representable g). lia. } unfold graph_to_mat. rewrite Znth_map, nat_inc_list_i. unfold vert_to_list. rewrite Znth_map. rewrite Znth_map. f_equal. f_equal. rewrite (combine_Znth (map (fun x : V => (src, x)) _ ) (nat_inc_list _) _). rewrite nat_inc_list_i, Znth_map, H1; trivial. rewrite <- Zlength_correct; trivial. rewrite map_length, nat_inc_list_length; trivial. rewrite Zlength_map; trivial. 2: rewrite Zlength_map. 1,2: rewrite Zlength_correct in *; rewrite (combine_length (map (fun x : V => (src, x)) _ ) (nat_inc_list _)), map_length, nat_inc_list_length, Nat.min_id; trivial. 2: rewrite nat_inc_list_Zlength. 1,2: rewrite Z2Nat.id; trivial. Qed.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat compcert.lib.Integers compcert.common.Values compcert.export.Clightdefs VST.veric.mpred VST.zlist.sublist VST.floyd.field_at VST.floyd.coqlib3 VST.msl.iter_sepcon VST.msl.seplog CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathEdgeLabelGraph