Apply not_TwoRamseyProp_5_7_Power_5.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
5,
7,
prim4 5.
Apply TwoRamseyProp_atleastp_atleastp with
u5,
u5,
u8,
u7,
prim4 u5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with
u5.
Apply nat_In_atleastp with
u8,
u7 leaving 2 subgoals.
The subproof is completed by applying nat_8.
The subproof is completed by applying In_7_8.