proposition: Theorem alpha_nat_divides_k_ge_1 m : alpha_nat b k │ alpha_nat b m <-> k │ m.
proof: Proof. Proof using Hak. split. + intros H1. destruct (euclid m Hk) as (l & [ | n ] & E1 & E2). { exists l; lia. } rewrite Nat.add_comm in E1. generalize (alpha_nat_mnlk_eq _ _ E1); intros H2. rewrite <- nat2Zp_expo, <- nat2Zp_mult in H2. apply nat2Zp_divides in H2; auto. apply is_rel_prime_div_r in H2. 2: apply is_rel_prime_expo, is_gcd_sym, alpha_nat_coprime; auto. apply divides_le in H2. * apply alpha_nat_smono with (1 := Hb) in E2; lia. * apply alpha_nat_gt_0; lia. + intros (l & Hl). generalize (alpha_nat_mnlk_eq 0 _ Hl); intros H2. rewrite <- nat2Zp_expo, <- nat2Zp_mult in H2. simpl in H2. rewrite nat2Zp_inj in H2. rewrite rem_of_0 in H2. generalize (div_rem_spec1 (alpha_nat b m) (alpha_nat b k)). exists (div (alpha_nat b m) (alpha_nat b k)); lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)