proposition: Lemma rotate_take_insert l s e i x: i < length l → rotate_take s e (<[i:=x]>l) = if decide (rotate_nat_sub s i (length l) < rotate_nat_sub s e (length l)) then <[rotate_nat_sub s i (length l):=x]> (rotate_take s e l) else rotate_take s e l.
proof: Proof. intros ?. unfold rotate_take. rewrite rotate_insert_r, insert_length by done. case_decide; [rewrite take_insert_lt | rewrite take_insert]; naive_solver lia. Qed.
imports: stdpp(options)