proposition: Lemma Vundef_cwedges_Zlength: forall n: Z, 0 <= n -> Zlength (Vundef_cwedges n) = n.
proof: Proof. intros. unfold Vundef_cwedges. apply Zlength_repeat. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist