Let x0 of type ι be given.
Apply SNo_recip_SNo_pos with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply recip_SNo_pos_pos with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply mul_SNo_nonzero_cancel with
recip_SNo_pos x0,
recip_SNo_pos (recip_SNo_pos x0),
x0 leaving 5 subgoals.
The subproof is completed by applying L2.
Apply SNoLt_irref with
0.
Apply H4 with
λ x1 x2 . SNoLt 0 x1.
The subproof is completed by applying L3.
Apply SNo_recip_SNo_pos with
recip_SNo_pos x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying H0.
Apply mul_SNo_com with
recip_SNo_pos x0,
x0,
λ x1 x2 . mul_SNo (recip_SNo_pos x0) (recip_SNo_pos (recip_SNo_pos x0)) = x2 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H0.
Apply recip_SNo_pos_invR with
x0,
λ x1 x2 . mul_SNo (recip_SNo_pos x0) (recip_SNo_pos (recip_SNo_pos x0)) = x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply recip_SNo_pos_invR with
recip_SNo_pos x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.