rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We prove the intermediate claim Li3i3: OSNo (i3 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i3 OSNo_Octonion_i3 OSNo_Octonion_i3.
We will prove i3 ⨯ i3 = - 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 (i3 ⨯ i3) (- 1) Li3i3 (HSNo_OSNo (- 1) L1) to the current goal.
We will prove p0 (i3 ⨯ i3) = p0 (- 1).
rewrite the current goal using HSNo_OSNo_proj0 (- 1) L1 (from left to right).
We will prove p0 (i3 ⨯ i3) = - 1.
rewrite the current goal using mul_OSNo_proj0 i3 i3 OSNo_Octonion_i3 OSNo_Octonion_i3 (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
We will prove 0 + - ((- i) ' * (- i)) = - 1.
rewrite the current goal using conj_minus_HSNo i HSNo_Complex_i (from left to right).
We will prove 0 + - ((- i ') * (- i)) = - 1.
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
We will prove 0 + - (i * (- i)) = - 1.
rewrite the current goal using minus_mul_HSNo_distrR i i HSNo_Complex_i HSNo_Complex_i (from left to right).
We will prove 0 + - - i * i = - 1.
rewrite the current goal using minus_HSNo_invol (i * i) (HSNo_mul_HSNo i i HSNo_Complex_i HSNo_Complex_i) (from left to right).
rewrite the current goal using Quaternion_i_sqr (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 (i3 ⨯ i3) = p1 (- 1).
rewrite the current goal using HSNo_OSNo_proj1 (- 1) L1 (from left to right).
We will prove p1 (i3 ⨯ i3) = 0.
rewrite the current goal using mul_OSNo_proj1 i3 i3 OSNo_Octonion_i3 OSNo_Octonion_i3 (from left to right).
We will prove p1 i3 * p0 i3 + p1 i3 * p0 i3 ' = 0.
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove (- i) * 0 + (- i) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
We will prove (- i) * 0 + (- i) * 0 = 0.
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎