1. FormalConjectures
  2. OEIS
  3. «340737»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Convergence of fraction numerators $a(n)/b(n)$ to $e$

a: Numerators of a sequence of fractions converging to $e$. $$a(1) = 3, a(2) = 5$$ For $n > 2$: $$a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - \left(\frac{n-2}{2}\right) a(n-3) & \text{if } n \text{ is even} \cr 2 a(n-1) + n a(n-2) & \text{if } n \text{ is odd} \end{cases}$$

References:

    A340737

    arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

    b

namespace OeisA340737open MeasureTheoryopen scoped Realopen Nat

Numerators of a sequence of fractions converging to $e$. $$a(1) = 3, a(2) = 5$$ For $n > 2$: $$a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - \left(\frac{n-2}{2}\right) a(n-3) & \text{if } n \text{ is even} \cr 2 a(n-1) + n a(n-2) & \text{if } n \text{ is odd} \end{cases}$$

def a (n : ℕ) : ℕ := match n with | 0 => 0 -- Required for total function, O(1,1) suggests 0 is not relevant. | 1 => 3 | 2 => 5 | n' + 3 => -- n $\ge$ 3 let n := n' + 3 let a_nm1 := a (n - 1) let a_nm2 := a (n - 2) let a_nm3 := a (n - 3) if n % 2 = 0 then -- n is even, n $\ge$ 4 let c1 : ℕ := (n + 2) / 2 let c2 : ℕ := (n - 2) / 2 -- $a(n) = c_1 \cdot a(n-1) - a(n-2) - c_2 \cdot a(n-3)$. -- We use Int.ofNat for safe subtraction, as the result is known to be positive. Int.toNat (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3) else -- n is odd, n $\ge$ 3 2 * a_nm1 + n * a_nm2 termination_by n

Denominators of a sequence of fractions converging to $e$. This sequence is defined by the same recurrence relation as a but with initial values $b(1)=1, b(2)=2$. $$b(1) = 1, b(2) = 2$$ For $n > 2$: $$b(n) = \begin{cases} \left(\frac{n+2}{2}\right) b(n-1) - b(n-2) - \left(\frac{n-2}{2}\right) b(n-3) & \text{if } n \text{ is even} \cr 2 b(n-1) + n b(n-2) & \text{if } n \text{ is odd} \end{cases}$$

def b (n : ℕ) : ℕ := match n with | 0 => 0 | 1 => 1 | 2 => 2 | n' + 3 => -- n $\ge$ 3 let n := n' + 3 let b_nm1 := b (n - 1) let b_nm2 := b (n - 2) let b_nm3 := b (n - 3) if n % 2 = 0 then -- n is even, n $\ge$ 4 let c1 : ℕ := (n + 2) / 2 let c2 : ℕ := (n - 2) / 2 -- $b(n) = c_1 \cdot b(n-1) - b(n-2) - c_2 \cdot b(n-3)$. -- We use Int.ofNat for safe subtraction. Int.toNat (Int.ofNat c1 * Int.ofNat b_nm1 - Int.ofNat b_nm2 - Int.ofNat c2 * Int.ofNat b_nm3) else -- n is odd, n $\ge$ 3 2 * b_nm1 + n * b_nm2 termination_by n@[category test, AMS 11] lemma a_1 : a 1 = 3 := ⊢ a 1 = 3 ⊢ 3 = 3; All goals completed! 🐙@[category test, AMS 11] lemma a_2 : a 2 = 5 := ⊢ a 2 = 5 ⊢ 5 = 5; All goals completed! 🐙@[category test, AMS 11] lemma a_3 : a 3 = 19 := ⊢ a 3 = 19 ⊢ (have n := 0 + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 19; ⊢ (have n := 0 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 19; ⊢ (have n := 0 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 19; All goals completed! 🐙@[category test, AMS 11] lemma a_4 : a 4 = 49 := ⊢ a 4 = 49 ⊢ (have n := 1 + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 49; ⊢ (have n := 1 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 49; ⊢ (have n := 1 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 49; ⊢ (have n := 1 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 49; All goals completed! 🐙@[category test, AMS 11] lemma a_5 : a 5 = 193 := ⊢ a 5 = 193 ⊢ (have n := 2 + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 193; ⊢ (have n := 2 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 193; ⊢ (have n := 2 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 193; ⊢ (have n := 2 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2) = 193; ⊢ (have n := 2 + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | ⋯ => 0 | ⋯ => 3 | ⋯ => 5 | ⋯ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | ⋯ => 0 | ⋯ => 3 | ⋯ => 5 | ⋯ => have n := n' + 3; have a_nm1 := match n - 1 with | ⋯ => 0 | ⋯ => 3 | ⋯ => 5 | ⋯ => have n := n' + 3; have a_nm1 := match n - 1 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm2 := match n - 2 with | 0 => 0 | 1 => 3 | 2 => 5 | n'.succ.succ.succ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - 3); if n % 2 = 0 then have c1 := (n + 2) / 2; have c2 := (n - 2) / 2; (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3).toNat else 2 * a_nm1 + n * a_nm2; have a_nm3 := match n - 3 with | ⋯ => 0 | ⋯ => 3 | ⋯ => 5 | ⋯ => have n := n' + 3; have a_nm1 := a (n - 1); have a_nm2 := a (n - 2); have a_nm3 := a (n - ⋯); ⋯; ⋯; ⋯; ⋯; ⋯) = ⋯; All goals completed! 🐙

Conjecture: $\lim_{n \to \infty} a(n) / b(n) = e$, where $b(n)$ is the companion denominator sequence.

A formal proof has been found with the methods described in arxiv/2605.22763.

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/340737.wip.lean#L438"] theorem tendsto_exp_one : Filter.Tendsto (fun n : ℕ => (a n : ℝ) / (b n : ℝ)) Filter.atTop (nhds (Real.exp 1)) := ⊢ Filter.Tendsto (fun n ↦ ↑(a n) / ↑(b n)) Filter.atTop (nhds (rexp 1)) All goals completed! 🐙end OeisA340737