proposition: Theorem recursion_0 : forall (A : Type) (a : A) (f : NN.t -> A -> A), recursion a f 0 = a.
proof: Proof. intros A a f; unfold recursion, NN.to_N; rewrite NN.spec_0; simpl; auto. Qed.
imports: ZArith OrdersFacts Nnat NAxioms NSig Lia