Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ octonion.
Let x1 of type ι be given.
Assume H1: x1 ∈ octonion.
Apply octonion_I with add_HSNo (OSNo_proj0 x0) (OSNo_proj0 x1), add_HSNo (OSNo_proj1 x0) (OSNo_proj1 x1) leaving 2 subgoals.
Apply quaternion_add_HSNo with OSNo_proj0 x0, OSNo_proj0 x1 leaving 2 subgoals.
Apply octonion_p0_quaternion with x0.
The subproof is completed by applying H0.
Apply octonion_p0_quaternion with x1.
The subproof is completed by applying H1.
Apply quaternion_add_HSNo with OSNo_proj1 x0, OSNo_proj1 x1 leaving 2 subgoals.
Apply octonion_p1_quaternion with x0.
The subproof is completed by applying H0.
Apply octonion_p1_quaternion with x1.
The subproof is completed by applying H1.
■