We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
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 Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li6i0: OSNo (i6 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i0 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i0) i2 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (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 + - (1 ' * (- j)) = j.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_id_SNo 1 SNo_1 (from left to right).
rewrite the current goal using mul_HSNo_1L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L j HSNo_Quaternion_j.
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (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 1 * 0 + (- j) * 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 mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎