proposition: Theorem peano_rec_succ P a f n : peano_rec P a f (succ n) = f n (peano_rec P a f n).
proof: Proof. apply peano_rect_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties