Apply unknownprop_adfc599b5be2c7d0b2fabccfee71b391794808bb6579ab39da7c767c7aa61f2d with
SNo,
add_SNo,
mul_SNo,
minus_SNo leaving 8 subgoals.
The subproof is completed by applying SNo_add_SNo.
The subproof is completed by applying mul_SNo_distrR.
The subproof is completed by applying mul_SNo_distrL.
The subproof is completed by applying SNo_minus_SNo.
The subproof is completed by applying SNo_mul_SNo.
The subproof is completed by applying mul_SNo_com.
The subproof is completed by applying mul_SNo_minus_distrR.
The subproof is completed by applying unknownprop_99a3c86e262d57a15068e53f2903d0677a958c45db7b2862850c06494aa7d66e.