proposition: Lemma drop_resize_le l n m x : n ≤ m → drop n (resize m x l) = resize (m - n) x (drop n l).
proof: Proof. revert n m. induction l; simpl. - intros. by rewrite drop_nil, !resize_nil, drop_replicate. - intros [|?] [|?] ?; simpl; try case_match; auto with lia. Qed.
imports: stdpp(options)