proposition: Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.
proof: Proof. reflexivity. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties