proposition: Lemma resize_app_ge l1 l2 n x : length l1 ≤ n → resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
proof: Proof. intros. rewrite !resize_spec, take_app_ge, (assoc_L (++)) by done. do 2 f_equal. rewrite app_length. lia. Qed.
imports: stdpp(options)