Apply not_TwoRamseyProp_atleast_3_6_Power_4.
Apply TwoRamseyProp_atleastp_atleastp with
5,
3,
7,
6,
prim4 4 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_In_atleastp with
5,
3 leaving 2 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying In_3_5.
Apply nat_In_atleastp with
7,
6 leaving 2 subgoals.
The subproof is completed by applying nat_7.
The subproof is completed by applying In_6_7.