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