Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: mul_SNo x0 x1 = 0.
Apply SNoLt_trichotomy_or_impred with x0, 0, or (x0 = 0) (x1 = 0) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Assume H3: SNoLt x0 0.
Apply SNoLt_trichotomy_or_impred with x1, 0, or (x0 = 0) (x1 = 0) leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying SNo_0.
Assume H4: SNoLt x1 0.
Apply FalseE with or (x0 = 0) (x1 = 0).
Apply SNoLt_irref with 0.
Apply H2 with λ x2 x3 . SNoLt 0 x2.
Apply mul_SNo_neg_neg with x0, x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying orIR with x0 = 0, x1 = 0.
Assume H4: SNoLt 0 x1.
Apply FalseE with or (x0 = 0) (x1 = 0).
Apply SNoLt_irref with 0.
Apply H2 with λ x2 x3 . SNoLt x2 0.
Apply mul_SNo_neg_pos with x0, x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying orIL with x0 = 0, x1 = 0.
Assume H3: SNoLt 0 x0.
Apply SNoLt_trichotomy_or_impred with x1, 0, or (x0 = 0) (x1 = 0) leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying SNo_0.
Assume H4: SNoLt x1 0.
Apply FalseE with or (x0 = 0) (x1 = 0).
Apply SNoLt_irref with 0.
Apply H2 with λ x2 x3 . SNoLt x2 0.
Apply mul_SNo_pos_neg with x0, x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying orIR with x0 = 0, x1 = 0.
Assume H4: SNoLt 0 x1.
Apply FalseE with or (x0 = 0) (x1 = 0).
Apply SNoLt_irref with 0.
Apply H2 with λ x2 x3 . SNoLt 0 x2.
Apply mul_SNo_pos_pos with x0, x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
■