proposition: Theorem alpha_Z_congr n : Z2Zp Hq (alpha_Z b1 n) = Z2Zp Hq (alpha_Z b2 n).
proof: Proof. Proof using Hb2 Hb1 Hb. induction on n as IHn with measure n. destruct n as [ | [ | n ] ]; try reflexivity. do 2 (rewrite alpha_fix_3; auto). do 2 rewrite Z2Zp_minus, Z2Zp_mult. do 2 f_equal; try (apply IHn; lia). do 2 (rewrite Z2Zp_pos; auto). do 2 rewrite Nat2Z.id; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)