proposition: Fact divides_mult_inv k p q : k <> 0 -> k*p div k*q -> p div q.
proof: Proof. intros H (n & Hn); exists n. apply Nat.mul_cancel_r with (1 := H). rewrite Nat.mul_comm, Hn; ring. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)