proposition: Theorem alpha_Z_b_2 n : 〚 alpha_Z b n 〛 = Zp_plus Hb 〚 Z.of_nat n 〛〚 -1 〛.
proof: Proof. rewrite <- Z2Zp_plus. replace (Z.of_nat n + -1) with (Z.of_nat n -1) by lia. rewrite <- (@alpha_2 2); auto. apply alpha_Z_congr; try lia. replace b with (2+(b-2))%nat at 3 by lia. rewrite nat2Zp_plus. rewrite nat2Zp_p, Zp_add_comm, Zp_plus_zero; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)