proposition: Theorem central_induction : forall z, A z -> (forall n, A n <-> A (S n)) -> forall n, A n.
proof: Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. - solve_proper. - intro; now apply bi_induction. - intro n; pose proof (Step n); tauto. Qed.
imports: NZAxioms