Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_HSNo (mul_HSNo (p0 z) (p0 w)) (minus_HSNo (mul_HSNo (conj_HSNo (p1 w)) (p1 z)))) (add_HSNo (mul_HSNo (p1 w) (p0 z)) (mul_HSNo (p1 z) (conj_HSNo (p0 w)))) ∈ octonion.
We prove the intermediate claim Lz0: p0 z ∈ quaternion.
An exact proof term for the current goal is octonion_p0_quaternion z Hz.
We prove the intermediate claim Lz1: p1 z ∈ quaternion.
An exact proof term for the current goal is octonion_p1_quaternion z Hz.
We prove the intermediate claim Lw0: p0 w ∈ quaternion.
An exact proof term for the current goal is octonion_p0_quaternion w Hw.
We prove the intermediate claim Lw1: p1 w ∈ quaternion.
An exact proof term for the current goal is octonion_p1_quaternion w Hw.
Apply octonion_I to the current goal.
Apply quaternion_add_HSNo to the current goal.
Apply quaternion_mul_HSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply quaternion_minus_HSNo to the current goal.
Apply quaternion_mul_HSNo to the current goal.
Apply quaternion_conj_HSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply quaternion_add_HSNo to the current goal.
Apply quaternion_mul_HSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply quaternion_mul_HSNo to the current goal.
An exact proof term for the current goal is ??.
Apply quaternion_conj_HSNo to the current goal.
An exact proof term for the current goal is ??.
∎