proposition: Fact rem_plus a b : rem (a+b) p = rem (rem a p + rem b p) p.
proof: Proof. rewrite (div_rem_spec1 a p) at 1. rewrite (div_rem_spec1 b p) at 1. apply rem_erase with (div a p + div b p). ring. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)