proposition: Theorem alpha_nat_mnlk_eq : 〚 alpha_nat b m 〛 = 〚 alpha_nat b n 〛⊗ expo l〚 alpha_nat b (1+k) 〛.
proof: Proof. Proof using Hm. generalize alpha_Z_mnlk_eq. simpl plus. unfold alpha_Z. do 3 (rewrite Z2Zp_pos; auto). do 3 rewrite Nat2Z.id; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)