proposition: Fact Zp_lprod_app l m : Zp_lprod (l++m) = Zp_lprod l ⊗ Zp_lprod m.
proof: Proof. induction l as [ | x l IHl ]. + rewrite Zp_lprod_nil, Zp_mult_one; auto. + simpl app; do 2 rewrite Zp_lprod_cons. rewrite IHl; ring. 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)