proposition: Lemma peano_ind (P : Z -> Prop) : P 0 -> (forall x, P x -> P (succ x)) -> (forall x, P x -> P (pred x)) -> forall z, P z.
proof: Proof. intros H0 Hs Hp z; destruct z as [|p|p]. - assumption. - induction p as [|p IHp] using Pos.peano_ind. + now apply (Hs 0). + rewrite <- Pos.add_1_r. now apply (Hs (pos p)). - induction p as [|p IHp] using Pos.peano_ind. + now apply (Hp 0). + rewrite <- Pos.add_1_r. now apply (Hp (neg p)). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass