proposition: Lemma BS : forall z : Z, B z -> B (z + 1).
proof: Proof. intros z H. unfold B in *. apply -> AS in H. setoid_replace (of_Z (z + 1)) with (succ (of_Z z)); auto. zify. auto. Qed.
imports: Bool ZArith OrdersFacts Nnat ZAxioms ZSig Lia