Let x0 of type ι be given.
Apply SNoLt_trichotomy_or_impred with
recip_SNo_pos x0,
0,
SNoLt 0 (recip_SNo_pos x0) leaving 5 subgoals.
Apply SNo_recip_SNo_pos with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying SNo_0.
Apply FalseE with
SNoLt 0 (recip_SNo_pos x0).
Apply SNoLt_irref with
0.
Apply SNoLt_tra with
0,
1,
0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNoLt_0_1.
Apply recip_SNo_pos_invR with
x0,
λ x1 x2 . SNoLt x1 0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply mul_SNo_pos_neg with
x0,
recip_SNo_pos x0 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply SNo_recip_SNo_pos with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply FalseE with
SNoLt 0 (recip_SNo_pos x0).
Apply neq_1_0.
Apply recip_SNo_pos_invR with
x0,
λ x1 x2 . x1 = 0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with
λ x1 x2 . mul_SNo x0 x2 = 0.
Apply mul_SNo_zeroR with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.