proposition: Lemma rotate_insert_l l n i x: i < length l → rotate n (<[rotate_nat_add n i (length l):=x]> l) = <[i:=x]> (rotate n l).
proof: Proof. intros Hlen. pose proof (Nat.mod_upper_bound n (length l)) as ?. unfold rotate. rewrite insert_length, rotate_nat_add_add_mod, rotate_nat_add_alt by lia. remember (n `mod` length l) as n'. case_decide. - rewrite take_insert, drop_insert_le, insert_app_l by (rewrite ?drop_length; lia). do 2 f_equal. lia. - rewrite take_insert_lt, drop_insert_gt, insert_app_r_alt, drop_length by (rewrite ?drop_length; lia). do 2 f_equal. lia. Qed.
imports: stdpp(options)