proposition: Fact Zp_expo_invertible n x : Zp_invertible x -> Zp_invertible (mscal Zp_mult Op n x).
proof: Proof. intros; induction n; [ rewrite mscal_0 | rewrite mscal_S ]; 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)