Apply not_TwoRamseyProp_4_6_Power_5.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
4,
6,
prim4 5.
Apply TwoRamseyProp_atleastp_atleastp with
u5,
u4,
u6,
u6,
prim4 u5 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_In_atleastp with
u5,
u4 leaving 2 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying In_4_5.
The subproof is completed by applying atleastp_ref with
u6.