proposition: Lemma Zlength_cons_sub_1: forall A (a: A) l, Zlength (a :: l) - 1 = Zlength l.
proof: Proof. intros. rewrite Zlength_cons. pose proof (Zlength_nonneg l). lia. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver