proposition: Fact rem_mult_rem a b : rem (a*rem b p) p = rem (a*b) p.
proof: Proof. rewrite (div_rem_spec1 b p) at 2. rewrite Nat.mul_add_distr_l, Nat.mul_assoc. symmetry; apply rem_erase with (a*div b p); auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)