Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLe x0 0.
Assume H2: SNo x1.
Assume H3: SNo x2.
Assume H4: SNoLe x2 x1.
Apply SNoLtLe_or with x0, 0, SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Assume H5: SNoLt x0 0.
Apply SNoLtLe_or with x2, x1, SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2) leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Assume H6: SNoLt x2 x1.
Apply SNoLtLe with mul_SNo x0 x1, mul_SNo x0 x2.
Apply neg_mul_SNo_Lt with x0, x1, x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Assume H6: SNoLe x1 x2.
Apply SNoLe_antisym with x1, x2, λ x3 x4 . SNoLe (mul_SNo x0 x4) (mul_SNo x0 x2) leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H4.
The subproof is completed by applying SNoLe_ref with mul_SNo x0 x2.
Assume H5: SNoLe 0 x0.
Apply SNoLe_antisym with x0, 0, λ x3 x4 . SNoLe (mul_SNo x4 x1) (mul_SNo x4 x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply mul_SNo_zeroL with x1, λ x3 x4 . SNoLe x4 (mul_SNo 0 x2) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply mul_SNo_zeroL with x2, λ x3 x4 . SNoLe 0 x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying SNoLe_ref with 0.
■