proposition: Lemma Zseq_In: forall z x, In x (Zseq z) <-> 0 <= x < z.
proof: Proof. intros; unfold Zseq; simpl; split; intros. + destruct x; destruct z; try inversion H. lia. apply Coqlib.list_in_map_inv in H. destruct H. destruct H. rewrite in_seq in H0. lia. apply Coqlib.list_in_map_inv in H. destruct H. destruct H. assert (Z.neg p < 0) by (apply Pos2Z.neg_is_neg). assert (0 <= Z.of_nat x) by (apply Nat2Z.is_nonneg). lia. + destruct x; destruct z; try lia. apply (in_map Z.of_nat (seq 0 (Z.to_nat (Z.pos p))) 0%nat). rewrite in_seq. simpl. lia. rewrite <- positive_nat_Z. apply (in_map Z.of_nat (seq 0 (Z.to_nat (Z.pos p0))) (Pos.to_nat p)). rewrite in_seq. 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