proposition: Lemma lookup_resize_new l n x i : length l ≤ i → i < n → resize n x l !! i = Some x.
proof: Proof. intros ??. rewrite resize_ge by lia. replace i with (length l + (i - length l)) by lia. by rewrite lookup_app_r, lookup_replicate_2 by lia. Qed.
imports: stdpp(options)