Sqrt correct

theorem sqrt_correct (n : Nat) (cn : SKI) (hcn : IsChurch n cn) :    IsChurch (Nat.sqrt n) (Sqrt ⬝ cn) := by  apply isChurch_trans _ (sqrt_def cn)  apply RFind_correct (fun k => if n < (k + 1) * (k + 1) then 0 else 1) (SqrtCond ⬝ cn)  · -- SqrtCond ⬝ cn correctly computes the function    intro i y hy    apply isChurch_trans _ (sqrtCond_def cn y)    have hsucc := succ_correct i y hy    have hle := le_correct _ n _ cn (mul_correct hsucc hsucc) hcn    have hneg := neg_correct _ _ hle    apply isChurch_trans _ (cond_correct _ _ _ _ hneg)    grind  · -- fNat (Nat.sqrt n) = 0    simp [Nat.lt_succ_sqrt]  · -- ∀ i < Nat.sqrt n, fNat i ≠ 0    grind [Nat.le_sqrt]