proposition: Corollary alpha_nat_congruence_1 b n : b-2 <> 0 -> rem (alpha_nat b n) (b-2) = rem n (b-2).
proof: Proof. intros Hb. rewrite <- alpha_nat_2 with (b_nat := 2) (n := n) at 2; auto. apply alpha_nat_congruence_0; try lia. replace b with ((b-2)+2) at 1 by lia. apply rem_erase with 1; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)