proposition: Lemma resize_resize l n m x : n ≤ m → resize n x (resize m x l) = resize n x l.
proof: Proof. revert n m. induction l; simpl. - intros. by rewrite !resize_nil, resize_replicate. - intros [|?] [|?] ?; f_equal/=; auto with lia. Qed.
imports: stdpp(options)