proposition: Lemma sublist_lookup_alter_ne f l i j n k : sublist_lookup j n l = Some k → length (f k) = n → i + n ≤ j ∨ j + n ≤ i → sublist_lookup i n (sublist_alter f j n l) = sublist_lookup i n l.
proof: Proof. unfold sublist_lookup. intros Hk Hi ?. erewrite sublist_alter_length by eauto. unfold sublist_alter; simplify_option_eq; f_equal; rewrite Hk. apply list_eq; intros ii. destruct (decide (ii < length (f k))); [|by rewrite !lookup_take_ge by lia]. rewrite !lookup_take, !lookup_drop by done. destruct (decide (i + ii < j)). { by rewrite lookup_app_l, lookup_take by (rewrite ?take_length; lia). } rewrite lookup_app_r by (rewrite take_length; lia). rewrite take_length_le, lookup_app_r, lookup_drop by lia. f_equal; lia. Qed.
imports: stdpp(options)