have h: ∀ {H: List Unit} {a b c d e f: BitTree} [Perfect H a] [Perfect H a] [Perfect H b] [Perfect H c] [Perfect H d] [Perfect H e] [Perfect H f],
    (a.toNat H * b.toNat H + c.toNat H * d.toNat H + e.toNat H * f.toNat H) % (bound H * bound H * bound H * bound H) =
    a.toNat H * b.toNat H + c.toNat H * d.toNat H + e.toNat H * f.toNat H :=
  Nat.mod_eq_of_lt (add_lt_mul_bound
    (add_le_mul_bound
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _)))
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _))))
     (add_lt_mul_bound
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _)))
      (Nat.mul_lt_mul_for_real
        (bound_pos _)
        (bound_pos _))))
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
h :
  ∀ {H : List Unit} {a b c d e f : BitTree} [inst : Perfect H a] [inst : Perfect H a] [inst : Perfect H b]
    [inst : Perfect H c] [inst : Perfect H d] [inst : Perfect H e] [inst : Perfect H f],
    (toNat H a * toNat H b + toNat H c * toNat H d + toNat H e * toNat H f) % (bound H * bound H * bound H * bound H) =
      toNat H a * toNat H b + toNat H c * toNat H d + toNat H e * toNat H f
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi