rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We prove the intermediate claim Li5i5: OSNo (i5 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i5 OSNo_Octonion_i5 OSNo_Octonion_i5.
We will prove i5 ⨯ i5 = - 1.
We prove the intermediate claim L1: HSNo (- 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply OSNo_proj0proj1_split (i5 ⨯ i5) (- 1) Li5i5 (HSNo_OSNo (- 1) L1) to the current goal.
We will prove p0 (i5 ⨯ i5) = p0 (- 1).
rewrite the current goal using HSNo_OSNo_proj0 (- 1) L1 (from left to right).
We will prove p0 (i5 ⨯ i5) = - 1.
rewrite the current goal using mul_OSNo_proj0 i5 i5 OSNo_Octonion_i5 OSNo_Octonion_i5 (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
We will prove 0 + - ((- k) ' * (- k)) = - 1.
rewrite the current goal using conj_minus_HSNo k HSNo_Quaternion_k (from left to right).
We will prove 0 + - ((- k ') * (- k)) = - 1.
rewrite the current goal using conj_HSNo_k (from left to right).
We will prove 0 + - ((- - k) * (- k)) = - 1.
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
We will prove 0 + - (k * (- k)) = - 1.
rewrite the current goal using minus_mul_HSNo_distrR k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
We will prove 0 + - - (k * k) = - 1.
rewrite the current goal using Quaternion_k_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_HSNo_0L (- 1) L1.
We will prove p1 (i5 ⨯ i5) = p1 (- 1).
rewrite the current goal using HSNo_OSNo_proj1 (- 1) L1 (from left to right).
We will prove p1 (i5 ⨯ i5) = 0.
rewrite the current goal using mul_OSNo_proj1 i5 i5 OSNo_Octonion_i5 OSNo_Octonion_i5 (from left to right).
We will prove p1 i5 * p0 i5 + p1 i5 * p0 i5 ' = 0.
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove (- k) * 0 + (- k) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎