proposition: Fact is_rel_prime_div p q k : is_gcd p q 1 -> p div q*k -> p div k.
proof: Proof. intros H1 (u & H2); subst. destruct bezout_nc with (1 := H1) as (a & b & H3). replace k with (k*(1+p*q) - k*p*q). + apply divides_minus. - rewrite <- H3, Nat.mul_add_distr_l. apply divides_plus. * rewrite Nat.mul_assoc; auto. * rewrite (Nat.mul_comm b), Nat.mul_assoc, (Nat.mul_comm k), H2. rewrite Nat.mul_comm, Nat.mul_assoc; auto. - rewrite Nat.mul_comm, Nat.mul_assoc; auto. + rewrite Nat.mul_add_distr_l, Nat.mul_assoc. generalize (k*p*q); intros; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)