proposition: Fact rem_plus_div a b : divides p b -> rem a p = rem (a+b) p.
proof: Proof. Proof using Hp. intros (n & Hn); subst. rewrite <- rem_plus_rem. f_equal. rewrite <- rem_mult_rem, rem_diag, Nat.mul_0_r, rem_of_0; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)