proposition: Fact Zp_lprod_cons x l : Zp_lprod (x::l) = x ⊗ Zp_lprod l.
proof: Proof. trivial. 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)