proposition: Lemma lookup_rotate_r_Some l n i x: rotate n l !! i = Some x ↔ l !! rotate_nat_add n i (length l) = Some x ∧ i < length l.
proof: Proof. split. - intros Hl. pose proof (lookup_lt_Some _ _ _ Hl) as Hlen. rewrite rotate_length in Hlen. by rewrite <-lookup_rotate_r. - intros [??]. by rewrite lookup_rotate_r. Qed.
imports: stdpp(options)