proposition: Lemma B_holds : forall z : Z, B z.
proof: Proof. intros; destruct (Z_lt_le_dec 0 z). apply natlike_ind; auto with zarith. apply B0. intros; apply BS; auto. replace z with (-(-z))%Z in * by (auto with zarith). remember (-z)%Z as z'. pattern z'; apply natlike_ind. apply B0. intros; rewrite Z.opp_succ; unfold Z.pred; apply BP; auto. subst z'; auto with zarith. Qed.
imports: Bool ZArith OrdersFacts Nnat ZAxioms ZSig Lia