proposition: Theorem alpha_nat_divisibility_2 b k m : 2 <= b -> alpha_nat b k * alpha_nat b k │ alpha_nat b m <-> k*alpha_nat b k │ m.
proof: Proof. intros Hb. destruct k as [ | k ]. * simpl. destruct m as [ | m ]; try (simpl; tauto). split; intros H; apply divides_0_inv in H; try discriminate. contradict H; apply alpha_nat_gt_0; lia. * apply alpha_nat_divides_2_pos; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)