proposition: Lemma get_not_default_lt A (t:array A) x : t.[x] <> default t -> (x <? length t) = true.
proof: Proof. intros Hd. case_eq (x <? length t); intros Heq; [trivial | ]. elim Hd; rewrite get_out_of_bounds; trivial. Qed.
imports: Uint63