proposition: Theorem expo_congruence_Z n : nat2Zp Hm q ⊗〚α (S n)〛=〚α n〛⊕ nat2Zp Hm (power n q).
proof: Proof. Proof using Hb_nat. destruct Z2Zp_morph as [ G1 G2 G3 G4 G5 ]. generalize (AnVP n); intros H. apply M22_proj12 in H. rewrite Z2Zp_one in H. do 2 rewrite Zp_mult_one_r in H. rewrite expoZ_power in H. rewrite (Z2Zp_of_nat _ (power _ _)) in H. rewrite <- H, Z2Zp_of_nat. simpl plus; rewrite Z2Zp_opp; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)