proposition: Lemma Forall2_rotate n l k : Forall2 P l k → Forall2 P (rotate n l) (rotate n k).
proof: Proof. intros HAll. unfold rotate. rewrite (Forall2_length _ _ HAll). eauto using Forall2_app, Forall2_take, Forall2_drop. Qed.
imports: stdpp(options)