AlphaProof IMO 2024 P1 in LEAN 之 induction 策略（Tactic）

        在 AlphaProof 使用 intro 策略后，此时的目的（Goal）为：

        这时，AlphaProof 使用 induction 策略，对 n : ℕ 进行，归纳证明：

        induction 策略，在假设中，增加了，在归纳证明中使用的，前值假设，即：

        改写后的目的（Goal）的高亮部分，

a : ∀ m < n, ⌊(↑m + 1) * x⌋ = ⌊x⌋ + 2 * ↑m * (l - ⌊x⌋)

        其中，induction 策略定义如下：

        另，其 using 参数的定义如下：

        那么，

        的 ‹_›，实际上就是，intro 策略提出来的 binder，n : ℕ，因为，假设中，只有 n : ℕ 符合 using 参数的要求，即，其类型为 自然数（Nat）。