Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_CSNo (mul_CSNo (p0 z) (p0 w)) (minus_CSNo (mul_CSNo (conj_CSNo (p1 w)) (p1 z)))) (add_CSNo (mul_CSNo (p1 w) (p0 z)) (mul_CSNo (p1 z) (conj_CSNo (p0 w)))) ∈ quaternion.
We prove the intermediate claim Lz0: p0 z ∈ complex.
An exact proof term for the current goal is quaternion_p0_complex z Hz.
We prove the intermediate claim Lz1: p1 z ∈ complex.
An exact proof term for the current goal is quaternion_p1_complex z Hz.
We prove the intermediate claim Lw0: p0 w ∈ complex.
An exact proof term for the current goal is quaternion_p0_complex w Hw.
We prove the intermediate claim Lw1: p1 w ∈ complex.
An exact proof term for the current goal is quaternion_p1_complex w Hw.
Apply quaternion_I to the current goal.
Apply complex_add_CSNo to the current goal.
Apply complex_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_minus_CSNo to the current goal.
Apply complex_mul_CSNo to the current goal.
Apply complex_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_add_CSNo to the current goal.
Apply complex_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
Apply complex_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
∎