proposition: Theorem peano_rec_base P a f : peano_rec P a f 0 = a.
proof: Proof. apply peano_rect_base. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties