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 unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with x0, x1, λ x3 x4 . SNoLe x3 (mul_CSNo x0 x2) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with x0, x2, λ x3 x4 . SNoLe (mul_SNo x0 x1) x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply nonpos_mul_SNo_Le with x0, x1, x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.