proposition: Corollary alpha_square_nat : exists q, Zp_invertible Hak2 q /\ nat2Zp Hak2 (alpha_nat b m) = q ⊗ nat2Zp Hak2 l ⊗ nat2Zp Hak2 (alpha_nat b k).
proof: Proof. Proof using Hl Hm. exists (expoZp (l-1) (Z2Zp Hak2 (-1)) ⊗ expoZp (l-1) (Z2Zp Hak2 (alpha_Z b k))); split. + apply Zp_mult_invertible; apply Zp_expo_invertible. * apply Zp_opp_invertible. rewrite <- Z2Zp_opp. replace (- (-1))%Z with 1%Z by lia. rewrite Z2Zp_one. apply Zp_one_invertible. * destruct k; try lia; simpl. rewrite Z2Zp_of_nat. apply nat2Zp_invertible. unfold ak2. apply is_gcd_sym, is_rel_prime_mult; apply is_gcd_sym, alpha_nat_coprime; auto. + generalize alpha_Z_ml_eq; intros H. unfold alpha_Z in H at 1 2. do 2 rewrite Z2Zp_of_nat in H. rewrite H; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)