proposition: Fact divides_mult p q k : p div q -> p div k*q.
proof: Proof. intros (r & ?); subst. exists (k*r); rewrite Nat.mul_assoc; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)