proposition: Lemma list_find_app_Some l1 l2 i x : list_find P (l1 ++ l2) = Some (i,x) ↔ list_find P l1 = Some (i,x) ∨ length l1 ≤ i ∧ list_find P l1 = None ∧ list_find P l2 = Some (i - length l1,x).
proof: Proof. split. - intros ([?|[??]]%lookup_app_Some&?&Hleast)%list_find_Some. + left. apply list_find_Some; eauto using lookup_app_l_Some. + right. split; [lia|]. split. { apply list_find_None, Forall_lookup. intros j z ??. assert (j < length l1) by eauto using lookup_lt_Some. naive_solver eauto using lookup_app_l_Some with lia. } apply list_find_Some. split_and!; [done..|]. intros j z ??. eapply (Hleast (length l1 + j)); [|lia]. by rewrite lookup_app_r, Nat.add_sub' by lia. - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)]. + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|]. assert (i < length l1) by eauto using lookup_lt_Some. intros j y ?%lookup_app_Some; naive_solver eauto with lia. + rewrite list_find_Some, lookup_app_Some. split_and!; [by auto..|]. intros j y [?|?]%lookup_app_Some ?; [|naive_solver auto with lia]. by eapply (Forall_lookup_1 (not ∘ P) l1); [by apply list_find_None|..]. Qed.
imports: stdpp(options)