proposition: Lemma leb_length : forall A (t:array A), length t <=? max_length = true.
proof: Proof. intros A t. generalize (length t); clear t. intro i. rewrite leb_spec. apply Z.lt_succ_r. change (Z.succ (to_Z max_length)) with wB. apply to_Z_bounded. Qed.
imports: Int63 Psatz ZArith