Lemmas on when sums of natural numbers are less than their products

These are used when proving the subsum condition in the odd case.

theorem Nat.sum_le_prod {ι : Type u_1} {s : Finset ι} {f : ι → ℕ} (hf : ∀ i ∈ s, 2 ≤ f i) : ∑ i ∈ s, f i ≤ ∏ i ∈ s, f i

theorem Nat.add3_lt_mul3 {a b c : ℕ} (ha : 3 ≤ a) (hb : 3 ≤ b) (hc : 1 ≤ c) : a + b + c < a * b * c

The sum of three natural numbers is strictly less than their product if they are lower-bounded by 3, 3, 1 respectively.