proposition: Theorem alpha_nat_divisibility_1 b k m : 2 <= b -> alpha_nat b k │ alpha_nat b m <-> k │ m.
proof: Proof. intros Hb. destruct (eq_nat_dec k 0) as [ | Hk ]; subst. + simpl; split; intros H; apply divides_0_inv in H. - destruct (eq_nat_dec m 0) as [ | Hm ]; subst. * apply divides_0. * generalize (alpha_nat_gt_0 Hb Hm); lia. - subst; apply divides_0. + apply alpha_nat_divides_k_ge_1; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)