Apply not_TwoRamseyProp_5_6_Power_5.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
5,
6,
prim4 5.
Apply TwoRamseyProp_atleastp_atleastp with
u6,
u5,
u6,
u6,
prim4 u5 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_In_atleastp with
u6,
u5 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying In_5_6.
The subproof is completed by applying atleastp_ref with
u6.