Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply SNoLt_trichotomy_or_impred with x0, 0, or (x0 = 0) (SNoLt 0 (mul_SNo x0 x0)) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Assume H1: SNoLt x0 0.
Apply orIR with x0 = 0, SNoLt 0 (mul_SNo x0 x0).
Apply mul_SNo_neg_neg with x0, x0 leaving 4 subgoals.
The subproof is completed by applying H0.
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 orIL with x0 = 0, SNoLt 0 (mul_SNo x0 x0).
Assume H1: SNoLt 0 x0.
Apply orIR with x0 = 0, SNoLt 0 (mul_SNo x0 x0).
Apply mul_SNo_pos_pos with x0, x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H1.