proposition: Theorem peano_rect_succ P a f n : peano_rect P a f (succ n) = f n (peano_rect P a f n).
proof: Proof. destruct n; simpl. - trivial. - now rewrite Pos.peano_rect_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties