proposition: Theorem pred_succ : forall n, P (S n) == n.
proof: Proof. intro n. zify. rewrite <- pred_mod_wB. replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia