proposition: Lemma list_find_app_r l1 l2: list_find P l1 = None → list_find P (l1 ++ l2) = prod_map (λ x, x + length l1) id <$> list_find P l2.
proof: Proof. intros. apply option_eq; intros [j y]. rewrite list_find_app_Some. split. - intros [?|(?&?&->)]; naive_solver auto with f_equal lia. - intros ([??]&->&?)%fmap_Some; naive_solver auto with f_equal lia. Qed.
imports: stdpp(options)