We will prove pa 0 (minus_HSNo i) ∈ octonion.

Apply octonion_I to the current goal.

An exact proof term for the current goal is quaternion_0.

Apply quaternion_minus_HSNo to the current goal.

An exact proof term for the current goal is quaternion_i.

∎