Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

We will prove pa (add_HSNo (p0 z) (p0 w)) (add_HSNo (p1 z) (p1 w)) ∈ octonion.

Apply octonion_I to the current goal.

Apply quaternion_add_HSNo to the current goal.

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

An exact proof term for the current goal is octonion_p0_quaternion w Hw.

Apply quaternion_add_HSNo to the current goal.

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

An exact proof term for the current goal is octonion_p1_quaternion w Hw.

∎