proposition: Lemma Z_inc_list_length: forall n, Zlength (Z_inc_list n) = Z.of_nat n.
proof: Proof. intros. induction n. trivial. simpl Z_inc_list. rewrite Zlength_app. rewrite IHn. rewrite Nat2Z.inj_succ. unfold Zlength. simpl. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon