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 Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
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 Li4i2: OSNo (i4 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i2 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i2) (:-: 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 i4 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove k * j + - (0 ' * 0) = - i.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (k * j) (HSNo_mul_HSNo k j HSNo_Quaternion_k HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is Quaternion_k_j.
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 i4 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * k + 0 * j ' = - 0.
rewrite the current goal using mul_HSNo_0L (j ') (HSNo_conj_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎