proposition: Lemma nth_error_Znth {A} `{Ia : Inhabitant A}: forall (L1 L2 : list A) i j, 0 <= i < Zlength L1 -> 0 <= j < Zlength L2 -> nth_error L1 (Z.to_nat i) = nth_error L2 (Z.to_nat j) <-> Znth i L1 = Znth j L2.
proof: Proof. intros. assert (Z.to_nat i < length L1 /\ Z.to_nat j < length L2)%nat. { generalize (Zlength_length _ L1 (Zlength L1)); intro. generalize (Zlength_length _ L2 (Zlength L2)); intro. destruct H1. apply Zlength_nonneg. destruct H2. apply Zlength_nonneg. rewrite (H1 eq_refl). rewrite (H2 eq_refl). lia. } repeat rewrite <- nth_Znth; trivial. generalize (nth_error_nth A Ia); intros. split; intros. do 2 (rewrite H2 in H3; try lia). inversion H3. congruence. rewrite H2. rewrite H2. congruence. lia. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model