Apply mul_SNo_nonzero_cancel with
1,
recip_SNo_pos 1,
1 leaving 5 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying neq_1_0.
Apply SNo_recip_SNo_pos with
1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNoLt_0_1.
The subproof is completed by applying SNo_1.
Apply mul_SNo_oneL with
1,
λ x0 x1 . mul_SNo 1 (recip_SNo_pos 1) = x1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply recip_SNo_pos_invR with
1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNoLt_0_1.