Apply unknownprop_ef33cbfa8a3c9641f06f8d746915bd9763e226741ee4bfa085ee8395985e7b61 with
SNo,
mul_SNo leaving 3 subgoals.
The subproof is completed by applying SNo_mul_SNo.
The subproof is completed by applying mul_SNo_assoc.
The subproof is completed by applying mul_SNo_com.