proposition: Theorem induction : forall A : N.t -> Prop, Proper (N.eq==>iff) A -> A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
proof: Proof. intros A A_wd A0 AS n; apply right_induction with 0; try assumption. - intros; auto; apply le_0_l. - apply le_0_l. Qed.
imports: Decidable NAxioms NZProperties