proposition: Lemma lookup_rotate_r l n i: i < length l → rotate n l !! i = l !! rotate_nat_add n i (length l).
proof: Proof. intros Hlen. pose proof (Nat.mod_upper_bound n (length l)) as ?. unfold rotate. rewrite rotate_nat_add_add_mod, rotate_nat_add_alt by lia. remember (n `mod` length l) as n'. case_decide. - by rewrite lookup_app_l, lookup_drop by (rewrite drop_length; lia). - rewrite lookup_app_r, lookup_take, drop_length by (rewrite drop_length; lia). f_equal. lia. Qed.
imports: stdpp(options)