proposition: Fact divides_rem_congr p q a b : divides p q -> rem a q = rem b q -> rem a p = rem b p.
proof: Proof. intros H1 H2. rewrite <- (divides_rem_rem a H1), <- (divides_rem_rem b H1). f_equal; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)