have h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2) := mul_lt_mul_of_lt_of_le h4 h2
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
⊢ False
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2)
⊢ False