proposition: Lemma resize_add l n m x : resize (n + m) x l = resize n x l ++ resize m x (drop n l).
proof: Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. - by rewrite Nat.add_0_r, (right_id_L [] (++)). - by rewrite replicate_add. Qed.
imports: stdpp(options)