proposition: Fact rem_erase q n p r : q = n*p+r -> rem q p = rem r p.
proof: Proof. destruct (eq_nat_dec p 0) as [ | Hp ]; subst. + rewrite Nat.mul_comm, rem_0, rem_0; auto. + destruct (div_full r p) as (m & r' & H1 & H2). specialize (H2 Hp). rewrite rem_prop with r p m r'; auto. intros; apply rem_prop with (n+m); auto. rewrite Nat.mul_add_distr_r; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)