proposition: Lemma lookup_rotate_l l n i: i < length l → rotate n l !! rotate_nat_sub n i (length l) = l !! i.
proof: Proof. intros ?. rewrite lookup_rotate_r, rotate_nat_add_sub;[done..|]. apply rotate_nat_sub_lt. lia. Qed.
imports: stdpp(options)