proposition: Fact lprod_ge_1 l : Forall prime l -> 1 <= lprod l.
proof: Proof. induction 1 as [ | x l H IH ]; simpl; auto. change 1 with (1*1) at 1; apply Nat.mul_le_mono; auto. apply prime_ge_2 in H; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)