proposition: Theorem peano_case : forall P:positive -> Prop, P 1 -> (forall n:positive, P (succ n)) -> forall p:positive, P p.
proof: Proof. intros; apply peano_ind; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef