proposition: Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
proof: Proof. intros ??. destruct (decide (n < length l)). - by rewrite resize_le, lookup_take by lia. - by rewrite resize_ge, lookup_app_l by lia. Qed.
imports: stdpp(options)