proposition: Corollary Zseq_Zlength: forall z, 0 <= z -> Zlength (Zseq z) = z.
proof: Proof. intros. unfold Zseq. rewrite (Zlength_map nat Z Z.of_nat (seq 0 (Z.to_nat z))). rewrite Zlength_correct. rewrite seq_length. apply Z2Nat.id. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph