We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li0i3: OSNo (i0 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i3 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i3) (:-: i1) ?? (OSNo_minus_OSNo i1 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i1 ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 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 OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - ((- i) ' * 1) = - i.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo i HSNo_Complex_i (from left to right).
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 * 1) = - i.
rewrite the current goal using mul_HSNo_1R i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i).
rewrite the current goal using minus_OSNo_proj1 i1 ?? (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 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 OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove (- i) * 0 + 1 * 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 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
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.
∎