fact: Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A) := fix go l := match l with | [] => None | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l end.
imports: stdpp(options)