proposition: Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1).
proof: Proof. intros z H1 H2. unfold B in *. apply -> AS in H2. setoid_replace (N_of_Z (z + 1)) with (succ (N_of_Z z)); auto. unfold eq. rewrite spec_succ, 2 spec_N_of_Z; auto with zarith. Qed.
imports: ZArith OrdersFacts Nnat NAxioms NSig Lia