test_home_finder.lean

import home_finder
-- lemma real_big : (3000 : ℝ) + 2 > 50 := by norm_num
-- lemma a :ℕ := 7
-- lemma b :ℕ := a

#vind_home pell.xn
#vind_home pell.n_lt_a_pow


-- def recfn : ℕ → ℕ
-- | 0 := 0
-- | (n+1) := n

-- #vind_home recfn