proposition: Lemma default_make A (a : A) size : default (make size a) = a.
proof: Proof. assert (irr_lt : length (make size a) <? length (make size a) = false). { destruct (Uint63.ltbP (length (make size a)) (length (make size a))); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. } assert (get_make := get_make A a size (length (make size a))). rewrite !get_out_of_bounds in get_make; assumption. Qed.
imports: Uint63