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