proposition: Fact rem_rem x m : rem (rem x m) m = rem x m.
proof: Proof. destruct (eq_nat_dec m 0). + subst; rewrite !rem_0; auto. + apply rem_idem, div_rem_spec2; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)