constructor
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x) ∧ Odd (f n)
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x)

case right
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (f n)