proposition: Theorem expo_congruence n : (0 < n)%nat -> nat2Zp Hm (q * alpha_nat n) = nat2Zp Hm (alpha_nat (n-1) + power n q).
proof: Proof. Proof using Hb_nat. destruct n as [ | n ]; try lia. replace (S n-1)%nat with n by lia. rewrite nat2Zp_mult. generalize (expo_congruence_Z (S n)); intros H. do 2 rewrite alpha_Z_S in H. do 2 rewrite Z2Zp_of_nat in H. rewrite H, nat2Zp_plus; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)