proposition: Fact divides_rem_rem p q a : divides p q -> rem (rem a q) p = rem a p.
proof: Proof. destruct (eq_nat_dec p 0) as [ Hp | Hp ]. { intros (k & ->); subst; rewrite Nat.mul_0_r. repeat rewrite rem_0; auto. } intros H. generalize (div_rem_spec1 a q); intros H1. destruct H as (k & ->). rewrite H1 at 2. rewrite Nat.add_comm. apply rem_plus_div; auto. do 2 apply divides_mult. apply divides_refl. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)