proposition: Fact prime_div_mult p x y : prime p -> p <d x*y -> p <d x \/ p <d y.
proof: Proof. intros H1 H2. destruct (prime_gcd x H1); auto. right; revert H H2; apply is_rel_prime_div. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)