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