proposition: Fact nat2Zp_mult u v :〚u*v〛=〚u〛⊗〚v〛.
proof: Proof. apply Zp_inj; simpl. rewrite rem_mult_rem, (Nat.mul_comm (rem _ _)), rem_mult_rem. f_equal; 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)