proposition: Fact divides_mult_r p q k : p div q -> p div q*k.
proof: Proof. rewrite Nat.mul_comm; apply divides_mult; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)