proposition: Lemma length_make : forall A size (a:A), length (make size a) = if size <=? max_length then size else max_length.
proof: Proof. intros A size a. unfold length, make. replace (size <=? max_length) with true. reflexivity. symmetry. 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