proposition: Fact prime_in_decomp p l : prime p -> Forall prime l -> p <d lprod l -> In p l.
proof: Proof. intros H1. induction 1 as [ | x l Hl IHl ]; simpl; intros H2. + apply divides_1_inv in H2; apply (proj1 H1); auto. + destruct (prime_gcd x H1) as [ H3 | H3 ]. apply is_rel_prime_div with (1 := H3) in H2; auto. apply (proj2 Hl) in H3. destruct H3 as [ H3 | H3 ]; auto. contradict H3;apply H1. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)