proposition: Fact nat2Zp_expo n u : 〚mscal mult 1%nat n u〛 = mscal Zp_mult Zp_one n 〚u〛.
proof: Proof. induction n as [ | n IHn ]. + do 2 rewrite mscal_0; auto. + do 2 rewrite mscal_S. rewrite nat2Zp_mult, IHn; auto. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)