proposition: Lemma Z_inc_list_eq: forall i len, 0 <= i < (Z.of_nat len) -> i = Znth i (Z_inc_list len).
proof: Proof. intros. generalize dependent i. induction len. 1: intros; exfalso; destruct H; rewrite Nat2Z.inj_0 in H0; lia. intros. simpl. rewrite Nat2Z.inj_succ in H. destruct H. apply Zlt_succ_le in H0. apply Zle_lt_or_eq in H0. destruct H0. - rewrite app_Znth1. apply IHlen. lia. now rewrite Z_inc_list_length. - rewrite app_Znth2 by (rewrite Z_inc_list_length; lia). rewrite H0 at 2. rewrite Z_inc_list_length. simpl. replace (Z.of_nat len - Z.of_nat len) with 0 by lia. rewrite Znth_0_cons; trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon