proposition: Lemma to_list_In : forall {A} (t: array A) i, i <? length t = true -> In (t.[i]) (to_list t).
proof: Proof. intros A t i; assert (Bt := to_Z_bounded (length t)); assert (Bi := to_Z_bounded i); rewrite ltb_spec; unfold to_list. rewrite <- in_rev. apply foldi_ind. rewrite leb_spec, to_Z_0; lia. rewrite to_Z_0; lia. intros j l _; assert (Bj := to_Z_bounded j). rewrite ltb_spec; intros Hj IH. rewrite to_Z_add_1_wB by lia; intro Hij. case (reflect_eqb j i); [ intro Heq; rewrite Heq; clear Heq | rewrite <- to_Z_eq; intro Hneq ]. apply in_eq. apply in_cons. apply IH. lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz