English
In a semigroup with identity, the go part of the binary exponentiation recursor satisfies npowBinRec.go(k+1) m n = m · npowRec'(k+1) n.
Русский
В полугруппе с единицей, часть go рекурсора бинарного возведения в степень удовлетворяет: go(k+1) m n = m · npowRec'(k+1) n.
LaTeX
$$$\\text{npowBinRec.go} (k+1)\\, m\\, n = m \\cdot npowRec'(k+1)\\, n$$$
Lean4
@[to_additive]
theorem go_spec {M : Type*} [Semigroup M] [One M] (k : ℕ) (m n : M) :
npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n :=
by
unfold go
generalize hk : k + 1 = k'
replace hk : k' ≠ 0 := by omega
induction k' using Nat.binaryRecFromOne generalizing n m with
| zero => simp at hk
| one => simp [npowRec']
| bit b k' k'0 ih =>
rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
rw [npowRec'_succ (by cutsat), npowRec'_two_mul, ← npowRec'_two_mul, ← npowRec'_mul_comm (by cutsat), mul_assoc]
