Let z be given.

Assume Hz.

We will prove pa (conj_HSNo (p0 z)) (minus_HSNo (p1 z)) ∈ octonion.

Apply octonion_I to the current goal.

Apply quaternion_conj_HSNo to the current goal.

An exact proof term for the current goal is octonion_p0_quaternion z Hz.

Apply quaternion_minus_HSNo to the current goal.

An exact proof term for the current goal is octonion_p1_quaternion z Hz.

∎