fact: Definition peano_rect (P : N -> Type) (f0 : P 0) (f : forall n : N, P n -> P (succ n)) (n : N) : P n := let P' p := P (pos p) in let f' p := f (pos p) in match n with | 0 => f0 | pos p => Pos.peano_rect P' (f 0 f0) f' p end.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties