Category "induction"

Prove recursive function exists using only `nat_ind`

I'm trying to prove the following in Coq: ∀ B: Type, ∀ a: B, ∀ b: nat -> B -> B, ∃ f: nat -> B, f 0 = a ∧ ∀ n: na