proposition: Lemma Forall2_rotate_take s e l k : Forall2 P l k → Forall2 P (rotate_take s e l) (rotate_take s e k).
proof: Proof. intros HAll. unfold rotate_take. rewrite (Forall2_length _ _ HAll). eauto using Forall2_take, Forall2_rotate. Qed.
imports: stdpp(options)