∀ (x x_1 : ONote),
  x.mul x_1 =
    match x, x_1 with
    | ONote.zero, x => 0
    | x, ONote.zero => 0
    | o₁@h:(e₁.oadd n₁ a₁), e₂.oadd n₂ a₂ => if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ (o₁.mul a₂)