proposition: Theorem alpha_nat_congruence_0 b1 b2 q n : 2 <= b1 -> 2 <= b2 -> rem b1 q = rem b2 q -> rem (alpha_nat b1 n) q = rem (alpha_nat b2 n) q.
proof: Proof. intros H1 H2 H3. destruct (eq_nat_dec q 0) as [ H4 | H4 ]. + subst; do 2 rewrite rem_0 in H3; subst; auto. + rewrite <- nat2Zp_inj with (Hp := H4) in H3. apply alpha_Z_congr with (n := S n) in H3; auto. simpl in H3. do 2 rewrite Z2Zp_of_nat in H3. rewrite nat2Zp_inj in H3. trivial. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)