proposition: Lemma Forall2_resize_r l k x y n m : P x y → Forall (P x) k → Forall2 P l (resize n y k) → Forall2 P (resize m x l) (resize m y k).
proof: Proof. intros. destruct (decide (m ≤ n)). { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. } assert (n = length l); subst. { by rewrite (Forall2_length l (resize n y k)), resize_length. } rewrite (Nat.le_add_sub (length l) m), !resize_add, resize_all, drop_all, resize_nil by lia. auto using Forall2_app, Forall2_replicate_l, Forall_resize, Forall_drop, resize_length. Qed.
imports: stdpp(options)