Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

We will prove pa (add_CSNo (p0 z) (p0 w)) (add_CSNo (p1 z) (p1 w)) ∈ quaternion.

Apply quaternion_I to the current goal.

Apply complex_add_CSNo to the current goal.

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

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

Apply complex_add_CSNo to the current goal.

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

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

∎