proposition: Lemma sublist_lookup_compose l1 l2 l3 i n j m : sublist_lookup i n l1 = Some l2 → sublist_lookup j m l2 = Some l3 → sublist_lookup (i + j) m l1 = Some l3.
proof: Proof. unfold sublist_lookup; intros; simplify_option_eq; repeat match goal with | H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H end; rewrite ?take_drop_commute, ?drop_drop, ?take_take, ?Nat.min_l, Nat.add_assoc by lia; auto with lia. Qed.
imports: stdpp(options)