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