exact lemma_2 f hf _ h8 h7 hm3
case a.inr.inr.intro
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 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
h8 : f^[2] m2 = f^[↑(f m2)] m2
⊢ f m2 = m2
no goals